**Monadic second-order logic**describes theories with only one type*X*called the*base type*, and its powerset, Rel_{X}^{(1)}.**Full second-order logic**admits a list of base types, and the*full type of structures*of every kind over them. If there is only one base type*X*, these are Rel_{X}^{(n)}and Op_{X}^{(n)}for every*n*∈ℕ*. This allows quantifiers on all variable structures ranging over all structures of a chosen kind over base types.-
**Higher-order logic**allows more types which can be listed by construction order, from a list of base types to successively constructed types, either first-order or second-order constructions (which amount to a powerset or an exponentiation, done after a finitary product for arities >1).

We saw two natural second-order theories: arithmetic, and the concept of standard universe. Another one is geometry, which will be the object of section 6.

The concept of weak second-order theory can serve as the minimal basis of an incomplete formalization simulating second-order constructions and theories into first-order logic. What misses is the possibility to fully express by first-order axioms (beyond the case of finite sets), the wish that

∀(parameters), ∃*A*∈*P*, ∀*x*∈*X*,
*x* ∈ *A* ⇔ *F*(*x*, parameters).

The strength of this formalization depends on the chosen range of definability: what kind of formulas may

Only first-order logic has a clear, built-in concept of provability. Provability concepts for second-order logic can only be drawn from there, by conceiving provability for a second-order theory as given by that of some chosen first-order translated version of it. Stronger translations may induce a wider range of theorems than weaker ones.

But the direct use of

This is the most powerful *kind of* formalization for second-order logic,
giving it the whole proving power of set theory (in the sense of its converted
form as a first-order theory sketched in 1.10), but its precise power
depends on the specific version (axioms list) of set theory that is chosen. There is no end to the
possible power of set theories as sources of provability in second-order
logic, as more generally there can be no most powerful algorithmic
concept of proof for arithmetic (any good one can always be surpassed
by a better one, as the incompleteness theorem will show).

**Löwenheim-Skolem theorem**. Any first-order
theory with an infinite model, has multiple non-equinumerous ones, thus
is semantically incomplete.

Semantic completeness takes a more interesting sense for a second-order theory with an infinite model, interpreted in a fixed universe : the claim that all its

This makes direct sense in first-order logic, meaning that all models fall into a single class of elementary equivalence. The news is its meaningfulness for the main useful second order theories, i.e. its independence from the choice of first-order expression: logically incomplete theories in the sense of the weakest algorithm (with first-order definable structures) remain logically incomplete by any stronger ones (such as from axiomatic set theories), as their range of undecidable formulas (thus their range of elementary equivalence classes of models) can be shrinked but never eliminated, even among formulas which only use first-order types of variables.

- Each of bare arithmetic, Presburger arithmetic and geometry is both logically and semantically complete.
- First-order versions of them are semantically incomplete, with non-standard models elementarily equivalent but not isomorphic to standard ones.
- Full arithmetic and set theories are logically incomplete, though full arithmetic is semantically complete.

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Set theory (continued)

3. Algebra 1

4. Arithmetic and first-order foundations

5.1. Second-order structures and invariants

5.2.**Second-order logic**

5.3. Well-foundedness

5.4. Ordinals and cardinals

5.5. Undecidability of the axiom of choice

5.6. Second-order arithmetic

5.7. The Incompleteness Theorem

More philosophical notes :
5.2.

5.3. Well-foundedness

5.4. Ordinals and cardinals

5.5. Undecidability of the axiom of choice

5.6. Second-order arithmetic

5.7. The Incompleteness Theorem