5. Second-order foundations

5.1. Second-order structures and invariants
Second-order constructions
Second-order structures
Second-order invariants
Parametered subspaces
Dual types
Subspaces, embeddings and sections
5.2. 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
5.3. Well-foundedness
Well-founded relations
Transitive closure
Well-founded recursion
Models of set theory
Axiom of foundation
More needed axioms
5.4. Ordinals and cardinals
(not ready yet)

5.5. 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
5.6. 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
5.7. The Incompleteness Theorem
Self-quotation theorem
The Truth Undefinability Theorem
The Incompleteness Theorem
Löb's theorem