Second-order logic - monadic version and Henkin semantics

Solution 1:

In monadic second-order logic, formulas are only allowed to contain unary second-order variables and first-order variables. For example the formula $\psi$ $$\forall x \forall y \exists X~X(x, y)$$ is not a formula of monadic second-order logic, because it contains a binary second-order variable $X$. (Monadic second-order logic formulas are also not allowed to contain second-order functional variables).

In standard semantics, a structure consists of a domain and interpretations for non-logical symbols (as in first-order logic). A quantifier over an $n$-ary second-order variable is interpreted to range over all $n$-ary relations in the domain. Thus a formula $\exists X \phi(\bar a, \bar A)$ (where $X$ is an $n$-ary second-order variable) would be true in a structure ${\cal M} = (M, ...)$ iff there is a set $B \subseteq M^n$ such that $\phi(\bar a, \bar A, B)$ is true in $\cal M$.

Under the standard semantics even monadic second-order logic is expressive enough not to admit a recursive axiomatisation. It is widely known that the standard first-order Peano axioms together with the full induction axiom $$\forall P (P(0) \land \forall x (P(x) \to P(s(x))) \to \forall x P(x))$$ characterise the structure of natural numbers up to isomorphism. This means that the set of formulas that logically follow from these (finite number of) axioms is not arithmetical.

In contrast in Henking semantics, a structure explicitly specifies the universe over which quantifiers over $n$-ary second order variables should range. These are called Henkin prestructures. It is easy to find a formula that is valid in standard semantics, but whose negation admits a Henkin prestructure. For example the above formula $\psi$ is valid in standard semantics. But is false in a Henkin prestructure where the range of binary second-order variables is empty.

As Henkin prestructures are overly broad, one sometimes requires the universes of second-order variables to satisfy some comprehension axioms. That is certain definable subsets should be in the universe. According to SEP a Henkin prestructure where all comprehension axioms hold is called a Henkin structure. Carl Mummert notes that Henkin prestructures that do not satisfy all comprehension axioms are also often considered in mathematics (see his comment for more details).

Henkin semantics with any recursively enumerable set of comprehension axioms can be recursively axiomatised. This means that there a is formula $\chi$ that logically follows from Peano axioms together with full induction under standard semantics, but does not follow under Henkin semantics. This can be used to construct a valind (under standard semantics) formula, whose negation admits a Henkin structure.

More about Henkin semantics can be found in Stanford Encyclopedia of Philosophy