**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 all*second-order constructed*types from them, each of which is the set of all structures of a given kind with nonzero arity over them: from one base type*X*, these are Rel_{X}^{(n)}and Op_{X}^{(n)}for all*n*∈ℕ*. This means to allow quantifiers on variable structures over base types, but may also serve to conceive new kinds of structures.-
**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 (powerset or an exponentiation, to be done after a finitary product to serve arities >1).

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

Let us focus on the simple case of a unary relation on a second-order type

The role of type

- For a relation : ∀
*k*,*k*'∈*K*, (∀*x*_{1},...,*x*, (_{n}*x*_{1},...,*x*)∈_{n}*k*⇔ (*x*_{1},...,*x*)∈_{n}*k*') ⇒*k*=*k'* - For an operation :
∀
*k*,*k*'∈*K*, (∀*x*_{1},...,*x*,_{n}*k*(*x*_{1},...,*x*) =_{n}*k*'(*x*_{1},...,*x*)) ⇒_{n}*k*=*k'*

The concept of weak second-order theory can serve as an incomplete scheme for second-order constructions, translating second-order theories to first-order ones. What misses is the possibility to fully express by first-order axioms (beyond the case of finite sets), the wish that

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

While first-order logic has a clear concept of provability, second-order logic can only get one from there, that is the provability in a first-order translated version of a theory. Stronger options may give 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 proving power of set theory converted to a first-order theory (as in
1.10), but this power
depends on a chosen axiomatic set theory. There is no end to the possible
power of set theories as sources of provability in second-order logic, as (by
the incompleteness theorem) there can be no most powerful algorithmic
concept of proof for arithmetic : it is always possible to find better ones.

**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: theories which are logically incomplete by the weakest algorithm remain logically incomplete by any stronger ones, which may reduce the range of undecidability but never eliminate it.

- Presburger arithmetic and geometry are 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.1. Finiteness and countability

4.2. The Completeness Theorem

4.3. Non-standard models of Arithmetic

4.4. How theories develop

4.5.Second-order logic

4.6. Well-foundedness and ordinals

4.7. Undecidability of the axiom of choice

4.8. Second-order arithmetic

4.9. The Incompleteness Theorem