Basic logical notions.
Definitions in synthetic computability.
- Equivalent characterizations
Decidability of bounded quantifiers.
The product type for Nat is witnessing.
Division with Rest
Prime Numbers
Definition of First Order Logic in Coq
Full Syntax
Tarski Semantics
Natural Deduction
- Definition
- Soundness
Peano Arithmetic
- PA Axioms
- Robinson Arithmetic
- PA Models
  - Euclidean Lemma
  - Standard Model of PA
PA and Q are consistent in Coq.
Δ0 Formulas.
- Δ0 Completeness
- Δ0 Absolutness
- Σ1 Completeness
Overspill
Coding Lemmas
Church's Thesis
- CT_Q
- Strong part of the representability theorem.
- Weak part of the representability theorem.
Enumerable and discrete PA models have decidable divisibility.
Tennenbaum's Tehorem via a diagnoal argument.
HA-inseparable formulas.
Makholm's proof of Tennenbaum's Theorem.
Variants of Tennenbaum's theorem
- Tennenbaum via diagonal proof
- Tennenbaum via inseparable formulas
- Makholm's Variant
- McCarty's proof for the categoricity of HA.
Verification that all variants can be derived from WCT_Q.