From the little I've read about Henkin semantics for second-order logic, it seems like a fairly thin wrapper over the standard semantics for first-order logic. I'm wondering whether this impression is accurate and, if it is, whether it can be turned into a concrete translation procedure.

My question is twofold.

  • Can second-order logic with Henkin semantics be completely described by some structurally-inductive translation into many-sorted first-order logic?

  • Does the translation procedure below miss anything for the function-free fragment of second-order logic?

I'm especially curious about the small details and side conditions that a translation procedure would have to insist on, like whether predicates and functions in Henkin semantics are required to be extensionally unique. My translation procedure is intentionally naive and insists on no side conditions at all.

My question is similar to this question, but is different because it's specifically about the details and side-conditions that such a translation procedure would have to impose, if there are any.

For concreteness, for many-sorted first-order logic, I allow empty domains.

Also, I use $\color{blue}{\text{blue}}$ for the syntax of second-order logic.

For the syntax of second-order logic, I will use $\color{blue}{D}$ as the single first-order domain, and $\color{blue}{D^n \to 2}$ as the domain of $n$-ary predicates. $n$-ary functions will be handled via a paraphrase to $(n{+}1)$-ary predicates. My non-logical vocabulary consists of constant symbols and predicate symbols only.

I introduce a countable number of non-logical predicates $A^0, A^1, A^2, A^3 \cdots$ corresponding to $n$-ary predicate application. I assume that these symbols do not appear in the non-logical vocabulary of the second order theory in question

For the syntax of the fragment first-order logic that I'm targeting with the translation procedure, I will use $D$ as the sort corresponding to $\color{blue}{D}$, and $S^n$ as the sort corresponding to $\color{blue}{D^n \to 2}$.

First, I consider terms.

Because there are no function symbols, every term is a free variable, a bound variable, or a constant symbol. These are translated as is.

$$ \color{blue}{\mathrm{term}}^* =\!= \mathrm{term} $$

In order to handle predicates, I introduce the following predicate symbols in first-order logic denoting "predicate application" for predicate variables. Predicate symbols inherited from the procedure are left alone.

Suppose $\color{blue}{P}$ is a predicate symbol.

$$ \color{blue}{P(t_1, t_2, \cdots)}^* =\!= P^*(t_1^*, t_2^*, \cdots) $$

Suppose $\color{blue}{P}$ is a predicate variable of arity $n$. Let $A^n$ be a predicate of arity $\mathbf{n{+}1}$ of type $S^n \times D \times \cdots \times D \to 2$.

$$ \color{blue}{P(t_1, t_2, \cdots)}^* =\!= A^n(P^*, t_1^*, t_2^*, \cdots) $$

For a well-formed formula headed by a quantifier, just translate the sorts.

$$ \color{blue}{\left(\forall x : D \mathop. \varphi(x)\right)}^* =\!= \forall x : D \mathop. \varphi^*(x) $$

$$ \color{blue}{\left(\forall x : D^n \to 2 \mathop. \varphi(x)\right)}^* =\!= \forall x : S^n \mathop. \varphi^*(x) $$

For a well-formed formula headed by a connective, translate the connective.

$$ \color{blue}{(\varphi \land \psi)}^* =\!= \varphi^* \land \psi^* $$

$$ \color{blue}{(\lnot \varphi)}^* =\!= \lnot \varphi^* $$

A well-formed formula headed by equality is translated similarly.

$$ \color{blue}{(t_1 = t_2)}^* =\!= t_1^* = t_2^* $$

This translation of equality is intentionally naive. It's possible to recover extensionality of predicate symbols in a roundabout way by baking it into the translation of equality. This would map $\color{blue}{t_1 = t_2}$ to $(\forall x_1, x_2 \cdots : S^n \mathop. A^n(t_1, x_1, x_2, \cdots) \leftrightarrow A^n(t_2, x_1, x_2, \cdots) )$ where $\color{blue}{t_1, t_2}$ are of sort $\color{blue}{D^n \to 2}$. However, I'm trying to avoid resorting to tricks like this because it would make the mapping from SOL to FOL much more complicated.


1 Answer 1


Unless I'm reading too quickly, I think your question is answered at §9.1 of


with details spelt out at


  • 2
    $\begingroup$ I think SEP is dealing with problems like extensional uniqueness of predicates and functions and existence of definable predicates and functions by imposing constraints on the Henkin model itself ... rather than using an ordinary multi-sorted first-order model and imposing constraints at the syntactic level by changing the translation procedure. $\endgroup$ Commented Aug 22, 2021 at 19:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .