**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 allows quantifiers on variable structures ranging 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 5.

With only one involvement of a second-order type

- Those with target
*Y*are mere curried views of first-order structures; - Second-order structures given as evaluators in second-order constructions are "non-structuring" (like connectives and equality).

Elements of

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

- Enough structures to prevent any new symmetry: the above axiom
requests the evaluator to be «structuring enough» over
*K*to prevent, for any isomorphism between 2 models of*T*, any multiplicity of extensions to interpretations of*K*forming isomorphisms between extended models; - Not «enough axioms» to "define" (essentially determine) the extension
of the model, in the sense that, unlike in constructions, it does not ensure the
existence of an extension of any isomorphism to interpretations of
*K*; - Anyway not «too much axioms», so the theory remains consistent, with existing models.

The above 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*∈*K*, ∀*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.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

4.7. Ordinals and cardinals

4.8. Undecidability of the axiom of choice

4.9. Second-order arithmetic

4.10. The Incompleteness Theorem