# 5. Second-order foundations

5.1. Second-order structures and invariants
Second-order constructions

Second-order structures

Second-order invariants

Endomorphisms

Parametered subspaces

Dual types

Subspaces, embeddings and sections

Quotients

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
choiceHistorical 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

References

5.7. The
Incompleteness Theorem

Self-quotation theorem

The Truth Undefinability Theorem

The Incompleteness Theorem

Löb's theorem