Project Page Index Table of Contents
  • Definitions
  • Utilities
    • Translation between Classical and Intuitionistic Reasoning
    • Utilities on Robinson Arithmetic
    • Utilities for Formulas
  • Lemmas for Vectors
  • External Provability Predicates
    • Σ1-soundness
    • Definitions
    • Enumerability Facts
    • Construction of External Provability Predicates
  • Diagonal Lemma
    • Preliminary Definitions
    • Proof of the Diagonal Lemma
    • Counterexamples from Generalised Diagonal Lemma
  • Limitative Theorems
    • Indefinability
    • Tarski's Theorem
    • Gödel's First Incompleteness Theorem
  • Multivariate CT_Q
    • Premilinary Definitions
    • Substitution Lemmas
    • Proof of Multivariate CT_Q
    • Binary CT_Q
  • Löb's Theorem
    • Derivability Conditions
    • Proof of Löb's Theorem
    • Internal Löb's Theorem
    • Gödel's Second Incompleteness Theorem
  • Hilbert Systems
  • Equivalence Proof of Hilbert System and ND
    • Preliminary Facts
    • Compatibility Lemmas
    • Soundness Lemmas
    • Equivalence Proof
  • Mostowski Modification
    • Mostowski Modification for External Provability Predicates
    • Mostowski Modification for External Proof Predicates
  • Peano Arithmetic with Lists
    • Signature
    • Notations
    • Inclusion from PA Signature
    • Comparisons
  • Properties of PALI
    • List Axioms
    • Rewriting
  • Definition of Provability Predicate and Modus Ponens Proof
    • Definition of prov(x)
    • Boundedness Lemmas
    • Lemmas on the List Theory
    • Modus Ponens Rule
  • Partial Verification of the HBL conditions
    • Modus Ponens for Provability
    • Necessitation
Generated by coqdoc and improved with CoqdocJS