**Monadic second-order logic**describes theories with only two types: one type*X*, called the*base type*, and its powerset*P*(set of all unary relations on*X*).**Full second-order logic**admits one base type*X*, and any other types, each representing the set of all structures of a given kind over it (relations and operations with any arity): Rel_{X}^{(n)}and Op_{X}^{(n)}for any*n*∈ℕ*. More generally from several base types we can consider the sets of all structures of each kind between them (any number of arguments of each type, any type of results). By admitting such types for variables under quantifiers in formulas, this framework can be understood as allowing quantifiers over variable structures, which were not allowed by first-order logic. But it can also serve to conceive new kinds of structures as will be discussed below.-
**Higher-order logic**allows for further types, which can be enumerated ordered by construction: starting from a given list of base types, the next types are successive constructions from previous types, may they be first-order constructions, or second-order constructions as just mentioned. The construction of any kind of structures can be analyzed as a combination of that of the powerset with some first-order constructions (first some products, then subsets in the case of operations).

Let us focus on the simplest case (beyond second-order constants which are the first-order structures): that of a unary relation

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 above concept of weak second-order theory, as a pack of components to add to the first-order types, can serve as an incomplete scheme of construction of second-order types, to translate any second-order theories into a first-order one. What misses is the possibility, in the general case (for infinite sets), to fully express by first-order axioms the wish that

It can still be partially expressed by axioms stating that this type of structures contains all those somehow definable with parameters. In the case of the powerset they are called

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

The strength of such a formalization depends on a choice of "definability" concept: what kind of formulas may

As only first-order logic has a clear concept of formal provability, the only available concepts of provability for second-order theories are those of the first-order theories they can be converted to. Stronger conversion methods can eventually give a wider range of theorems than weaker ones.

Alternatively, formally admitting

The full power of first-order logic precisely using the involved types
(the base types plus the second-order ones, here *K*), admits formulas
*F* with bound second-order variables (= of type *K*) in the
comprehension axioms. This requirement on the interpretation
of *K* goes beyond any concept of «definable structures» of its kind
on the base types, and cannot be reduced to any property of its elements,
since its use of *K* in defining formulas makes
this condition for «being in *K*» circular.

Compared with Henkin semantics, this expands the range of expressible comprehension axioms by letting more kinds of variables in their formulas. Namely, comprehension axioms whose parameters may take any value in the universe and bound variables may range inside any set there, are implicitly given by the definition of the set builder symbol in our formalism. These make the interpretations of second-order types appear uniquely determined by those of the base type from the viewpoint of that set theory which sees its own universe as fixed (inside which any bijection on base types between 2 systems is uniquely extensible as an isomorphism of the second-order constructions from them), but a multiplicity of non-isomorphic interpretations re-appears from an external viewpoint where a diversity of non-standard universes is understood possible as shown by Skolem's paradox.

The formalization of set theory we introduced from the beginning to the powerset, the axiom of choice and the axiom of infinity (this essentially is Mac Lane set theory), is quite powerful and the most convenient to comfortably develop all ordinary mathematics. As a little step further, Zermelo set theory adds to this the once mentioned comprehension axioms with bound variables ranging over the universe itself. But much larger leaps in power will come from postulating the existence of more kinds of sets or other objects, starting with what may be abusively written (while ℘ is not a function) as the recursive sequence (℘According to the Löwenheim-Skolem theorem, first-order theories describing infinite systems cannot be semantically complete (first-order logic cannot prevent the coexistence of multiple non-isomorphic models that «incorrectly interpret the powerset», and thus would have different second-order properties if interpreted by the external «true powersets»).

A first-order theory will be called

Some semantically complete second-order theories (geometry, arithmetic with only addition and no multiplication) are already logically complete by the weakest method, as all models of this weakest first-order expression are elementarily equivalent (they have the same first-order expressible properties) though they are not isomorphic.

For other theories (full arithmetic, set theory), stronger methods will contribute to the provability of more formulas. However then, such a quest is usually endless: the logical incompleteness of these theories is fundamental in the sense that no fixed algorithm can ever suffice to decide all their formulas either (may this algorithm anyhow come from the rules of first-order logic, e.g. by a translation into some set theory, or not).

This is the name of the first-order theory we described as "with stable power type" to describe arithmetic. However the list of basic structures needs to be specified.

The following 3 presentations of second-order arithmetic as
first-order theories (with axioms lists implicitly determined by
the previous explanations) are equivalent (definable from each
other):

- With types ℕ and ℘(ℕ×ℕ) and with structures 0 and
*S*;

- With types ℕ and ℕ
^{ℕ}and with structures 0 and*S*;

- With types ℕ and ℘(ℕ) and with structures 0, + and ⋅ .

We get ℕ

Using ℕ

Using addition and multiplication we can define a bijection between ℕ and ℕ×ℕ by (

Most of mathematics (with some exceptions such as geometry, which
will be discussed later) uses one or both of

- The set ℕ of natural numbers. We characterized the theory of natural numbers as a second-order theory, i.e. using the powerset ℘(ℕ).
- The set ℝ of real numbers. It may be naturally characterized
using its own powerset ℘(ℝ); but it may also be built
from
*P*(ℕ) (i.e. there is a way to let ℘(ℕ) play the role of ℝ).

In fact, most of ordinary mathematics can be indirectly developed using only ℕ and

Most ordinary mathematics and all physics can be expressed in the theory of second order arithmetic expressed above.

The canonical bijection

But other encodings can be much more cumbersome (unnatural), so that this theoretical possibility to encode all ordinary mathematics into second-order arithmetic, while possible, is rather far-fetched and not practical as a way to study mathematics.

For example, arbitrary continuous function *f* from ℝ to ℝ
can be represented in *P*(ℕ×ℕ×ℕ×ℕ), and thus in *P*(ℕ),
by the set of 4-tuples of strictly positive natural numbers *a*,*b*,*c*,*d*
such that *f*(*a*/*b* − *b*/*a*) > *c*/*d*
− *d*/*c*.

Or, as another example of possible encoding, such that *f*(*a*
− *b*√2)
> *c* − *d*√2.

Set Theory and Foundations of Mathematics