Project Page Index Table of Contents
  • Basic logical notions.
  • Definitions in synthetic computability.
    • Equivalent characterizations
  • Division with Rest
  • Prime Numbers
  • Decidability of bounded quantifiers.
  • Nat and (Nat * Nat) are witnessing.
  • PA Models
    • Euclidean Lemma
    • Standard Model of PA
  • PA and Q are consistent in Coq.
  • Church's Thesis
    • CT_Q
    • Strong part of the representability theorem.
    • Weak part of the representability theorem.
  • Coding Lemmas
    • Coding in the standard model
    • Coding in an arbitrary model, up to some bound.
    • Coding in a non-standard model
  • Diagonal Proof of Tennenbaum's Theorem
    • Enumerable and discrete PA models have decidable divisibility.
    • Tennenbaum's Theorem via a diagnoal argument.
  • Tennenbaum's Teorem via inseparable predicates
    • Existence of inseparable predicates
    • Tennenbaum's Theorem via Inseparability
  • Makholms Proof of Tennenbaum's Theorem
  • McCarty Proof of Tennenbaum's Theorem
Generated by coqdoc and improved with CoqdocJS