**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, each of which is the set of all structures of that kind with nonzero arity over base types. 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. A full type of structures is said to be*second-order constructed*from base types, which differs from first-order constructions like the powerset differs from operators complying to the set generation principle.-
**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.

Second-order structures given as parts of constructions are "non-structuring" (like connectives and equality). Those with only one full type of structures as target are mere curried views of first-order structures.

In practice (for geometry), the only useful second-order structures are unary
relations on some full type of structures *Y*. First-order logic cannot express
the exhaustivity of *Y*, but can bypass *Y* to describe any unary relation
there as a type *P* meant as a subset of *Y*, and called a *type of structures*.
This will usually suffice, as the other side *Y*\*P* is not explicitly needed.

Elements of *P* are given their role as *n*-ary structures, by an
evaluator symbol *S* (whose kind is that
of those structures plus the argument of type *P* to be evaluated; its
curried view gives the intended injection from *P* to *Y*).
To reflect this role, *S*(*k*,
*x*_{1},...,*x _{n}*) will be abbreviated as
(

- For a relation : ∀
*k*,*k*'∈*P*, (∀*x*_{1},...,*x*, (_{n}*x*_{1},...,*x*)∈_{n}*k*⇔ (*x*_{1},...,*x*)∈_{n}*k*') ⇒*k*=*k'*(axiom of extensionality) - For an operation :
∀
*k*,*k*'∈*P*, (∀*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
*P*to prevent, for any isomorphism between 2 models of*T*, any multiplicity of extensions to interpretations of*P*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
*P*; - 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*∈*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.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