More generally from several base types we can consider the sets of all structures of any given kinds between them (numbers of arguments of each type, type of results). So the general idea of secondorder theories is that they can express, for any types X,Y of objects, formulas of the form «For every subset of X...», and thus also (equivalently) of the form «For every function from X to Y...».
Secondorder theories can be interpreted as firstorder theories, where each type K of structures receives its role by one structure symbol of that kind with one additional argument of type K, as explained in previous sections. Indeed, currying this symbol gives a function from K to the intended set of all such structures (the powerset or exponentiation). The obstacle against the full formalization of secondorder theories as firstorder theories, is that we cannot generally express the bijectivity of this function by axioms: its injectivity can be easily expressed in firstorder logic in the form of the below separation axiom, but its surjectivity can't.

∀k,k'∈K, (∀x_{1},...,x_{n},
S(k, x_{1},...,x_{n})
⇔ S(k', x_{1},..., x_{n}))
⇒ k = k' ∀k,k'∈K, (∀x_{1},...,x_{n}, S(k, x_{1},...,x_{n}) = S(k', x_{1},...,x_{n})) ⇒ k = k' 
Consider the case of a monadic secondorder theory (for example; other cases are similar). We shall express it as a firstorder theory with 2 types X, Y. In addition to the separation axiom, the idea that Y = P(X) will be expressed by a schema of axioms, called the comprehension axioms, expressing that all classes of elements of X (i.e. subsets of X defined by formulas with parameters in this theory, as in sections 1.5 and 1.7), belong to Y. They are written, for any formula F with at least one free variable of type X:
These axioms are essentially equivalent to those that defined the setbuilder we introduced for set theory (see 1.8, 1.11), except that this symbol is not needed (it can be seen as an abbreviation).
In fact, all comprehension axioms without quantifiers on Y
but only using bound variables in X and parameters in both
X and Y, are satisfied by taking as Y the
set of all classes of elements of X defined with
parameters in X only. (What about those using another
structure on Y in their defining formula ?)
So, what makes this construction more powerful than the previous
one, apart from the ability to use variables of type Y in
structures and other axioms, is the requirement to also admit in Y
all subsets of X defined using quantifiers on variables of
type Y. This goes beyond any concept of «definable subsets
of X», and cannot even be qualified as a property of these
subsets, since its use of Y in defining formulas makes
this condition of definability circular.
The expression of any theory inside set theory, initially
introduced in 1.3 for firstorder theories, can be extended to
secondorder theories, interpreting the notions of «all subsets»
and «all operations» by the powerset and exponentiation operators
of set theory. Then the rules of proof are those of set theory
once expressed as a firstorder theory (see 1.9, 1.10, 1.11).
This framework is the one expressing the intended meaning of
secondorder theories as deterministically involving the full set
of all structures of each given kind between given sets: the tools
of set theory ensure that this powerset will include all
structures that «can be found»; they interpret it in a model of
set theory which they implicitly regard as fixed (assuming that we
are «living in it»). However, since set theory is itself a
firstorder theory, this formal appearance of uniquely determining
these powersets is not real but simulated, as follows: from any
bijection between two sets X and X' we can define
the image in X' of any subset of X, which obliges
P(X) and P(X') to conform to each
other. Then, the view of diverse models of secondorder theories
as encompassed in a fixed model of set theory, obliges their
secondorder types to conform to each other when their base types
are in bijection. This correspondence between all considered
models gives the appearance of determination of secondorder types
from base types.
In this context, for a fixed X, any set Y with a
relation between X and Y, can be seen as a
relational system with language the set X of unary
relation symbols. In the category of such systems but only
accepting the embeddings as morphisms, the final objects are
those Y which are copies of the "true powerset" of X.
This method is the most powerful approach, as the available variables and tools for the defining formulas that can find subsets of X to bring into P(X), are extended much beyond the mere sets X and P(X), up to whatever range of other sets that this model of set theory may contain. However this is still not any kind of specific «most powerful formalization» because it is itself not fixed, as it depends on the choice of an axiomatic system for set theory, while there actually cannot be such a thing as «the most powerful axiomatic system for set theory» (we can always find a stronger one).
Higherorder theories generalize secondorder theories, by
having a list of types that can be enumerated starting from a
given list of base types, and successively making other types by
«secondorder constructions» from previous types, i.e.
constructions that may include not only products (as allowed by
the constructions of
firstorder logic), but also powerset («Y is the set
of all subsets of X») and exponentiation («Z is the
set of all functions from X to Y»). Saying that
they are successive constructions, means that there is an order
between types such that each type of objects said to be made of
«all the..» comes after those of which it is the powerset
or exponentiation.
Higherorder theories can be translated into secondorder theories
as follows. Take as the list of base types, all types that are
used in any construction of powerset or exponentiation. Then in
the secondorder theory over this list of base types, a good list
of structures and firstorder axioms will express all intended
relations between base types. Namely, the relation Y = P(X)
will be formalized by a structure of bijection between Y
and P(X).
This is the name of the firstorder 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 secondorder arithmetic as
firstorder theories (with axioms lists implicitly determined by
the previous explanations) are equivalent (definable from each
other):
For example, arbitrary continuous function f from ℝ to ℝ can be represented in P(ℕ×ℕ×ℕ×ℕ), and thus in P(ℕ), by the set of 4tuples 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.