5. Second-order foundations

Second-order constructions
Second-order structures
Second-order invariants
Endomorphisms
Parametered subspaces
Dual types
Subspaces, embeddings and sections
Quotients

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

Well-founded relations
Transitive closure
Well-founded recursion
Models of set theory
Axiom of foundation
More needed axioms

(not ready yet)

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

First-order arithmetic
Second-order arithmetic
Hierarchy of formulas
The diverse axioms using variable subformulas
Ordered list of the main axiomatic theories
References

Self-quotation theorem
The Truth Undefinability Theorem
The Incompleteness Theorem
Löb's theorem