# Second-order logic - monadic version and Henkin semantics

After looking at texts and Wikipedia, I am getting some confusion on difference between monadic second-order logic and full second-order logic and difference between Henkin semantic and full semantic.

Can anyone provide example sentences/formulae that clearly show the difference?

-

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

-
Be careful with your example, what you have written down is not a formula; essentially because $(x,y)$ is not an atomic formula. A formula capturing your idea is $\forall x \forall y \exists X (Xxy)$. – boumol May 12 '12 at 11:07
Another non-monadic formula is $(\exists f)(\forall z)[f(z) = z]$. Regarding Henkin models, in the most general setting they are not required to satisfy all comprehension axioms; that restriction is only needed if the axioms are also added to the object theory. For example a general Henkin model of $\mathsf{RCA}_0$ (a theory of arithmetic) will not satisfy the entire comprehension scheme. There is a completeness theorem for second order logic with Henkin semantics, but not if all the models are forced to satisfy the comprehension scheme. – Carl Mummert May 12 '12 at 11:49
The SEP does define Henkin models in which all the comprehension axioms have to hold, but that is because they are interested primarily in the philosophical study of second-order logic, and in that setting there is no reason not to include all the comprehension axioms. But in weak theories of arithmetic we generally do not include them all. – Carl Mummert May 12 '12 at 11:51
Maybe I misunderstood the question, but I thought he was asking for an explicit formula which is valid in monadic second order logic and is not valid in full Henkin semantics. Any idea how to write down one of these formulas? – boumol May 12 '12 at 12:07
@boumol There are hundreds of ways of defining formulas. I think $X(x, y)$ is much more common nowadays than $Xxy$ for atomic formulas. – Levon Haykazyan May 12 '12 at 20:02