# 4. Model Theory

4.1. Finiteness and countability
Axiom of infinity
Finite cardinalities Countability of ℕ×ℕ
Countability of finite sequences of integers
Rebuilding recursion
4.2. The Completeness Theorem
Existence of countable term algebras
Interpretation of first-order formulas
The Completeness Theorem
4.3. Non-standard models of Arithmetic
Standard and non-standard numbers
Existence of non-standard models
Non-standard models of bare arithmetic
Non-standard models of Presburger Arithmetic
Non-standard models of full first-order arithmetic
4.5. How mathematical theories develop
Development levels : proofs, definitions, constructions
The Galois connection (Mod,Tru)
Definitions
How definitions preserve models
4.4. Constructions
Construction schemes
A development scheme at each level looks like a component at the next level
How constructions preserve isomorphisms
4.6. Second-order logic
Second-order logic and its variants
Second-order structures, extensionality and effectiveness axiom
Translating second-order theories into first-order ones
Using first-order axiom schemas (weakest method)
The theory with stable power type (Henkin semantics)
Set theoretical interpretations (strongest method)
Semantic completeness, Löwenheim-Skolem theorem
logical completeness
4.7. Well-foundedness
Well-founded relations
Transitive closure
Well-founded recursion
Models of set theory
Axiom of foundation
More needed axioms
4.8. Ordinals and cardinals

4.9. Undecidability of the axiom of choice
Historical note
Well-ordering and the axiom of choice
Rebuilding recursion - Proving the finite choice theorem
Axiom of dependent choice (DC)
Injections of ℕ into infinite sets
Counter-examples to the axiom of choice
AC vs measurability
4.10. Second-order arithmetic
First-order arithmetic
Second-order arithmetic
Hierarchy of formulas
The diverse axioms using variable subformulas
Ordered list of the main axiomatic theories
References
4.11. The Incompleteness Theorem
Self-quotation theorem
The Truth Undefinability Theorem
The Incompleteness Theorem
Löb's theorem