When does Skolemization require the axiom of choice?

Question

Skolemization is often used for eliminating existential quantifiers, which is often useful for proving theorems, especially in automated resolution theorem proving. Skolemization in first order predicate calculus is often based on a second order identity:

$\forall$x$\exists$y $\phi$(x,y) $\iff$ $\exists$f$\forall$x $\phi$(x, f(x))

I asked on the math.stackexchange site how to perform this operation in higher order logic, with a reasonably satisfactory answer, with one rather large caveat.

Apparently, at higher levels of logic, exploiting this identity to use an operation like Skolemization to eliminate existential quantifiers requires the axiom of choice. Is this always the case? This seems like a fairly heavy assumption for using a proof calculus, so are there any restricted forms of higher order Skolemization or existential quantifier elimination that don't require the axiom of choice, or require weaker versions of choice like countable choice or dependent choice?

Answer 1

Upon rereading the question, I sense there may be a terminological or conceptual confusion in play.

The terms “second-order logic” and “higher-order logic” are unfortunately used to denote two vastly different things:

1. Proper second/higher-order logic. This is a semantically defined system; its models consist of a first-order structure to interpret the first-order sort, which is canonically expanded to higher sorts by taking power sets and/or sets of all functions with appropriate domains (depending on the exact language). In this case, validity of the $$\tag{$*$}\forall x\,\exists y\,\phi(x,y) \leftrightarrow \exists f\,\forall x \,\phi(x, f(x))$$ schema in this logic is equivalent to the axiom of choice, as noted in Asaf’s answer. This is not limited to the axiom of choice: a substantial number of other set-theoretic principles (e.g., (non)existence of various large cardinals) are equivalent to validity of particular formulas in second-order logic, so this logic is effectively set theory in disguise. For much the same reasons, it has no proof system (its complexity is much higher than recursively enumerable).

2. Various first-order theories formulated in the multi-sorted language of second/higher-order logic. The fact that the question refers to “proof calculus” strongly suggests that this is the intended meaning here.

   In this case, the schema $(*)$ is just a convenient axiom that one might or might not choose to adopt in a particular system. The fact that it may be invalid in “standard models” as in 1. if the axiom of choice fails is neither here nor there: the logic is in any case not complete with respect to standard models, and there is no particular need for it to be sound either.

   Since these theories are generally recursively axiomatized, typical questions about their proof-theoretic properties (e.g., whether including the choice schema $(*)$ significantly strengthens a given system, or whether it is conservative for some class of formulas) are arithmetical statements of low quantifier complexity. As such, they are absolute, and in particular, they do not depend on whether the axiom of choice holds in the metatheory.

   However: to further terminological confusion, the schema $(*)$ is itself called the axiom of choice in the context of these logics. So, it is not actually clear to me what you are asking about: does the “require the axiom of choice” in the last paragraph of the question refer to the axiom of choice in metatheory, or to the schema $(*)$?

---

Let me also give a possible answer to a possible reading of the question. Systematic application of skolemization makes any formula equivalent to an $\exists\forall$ formula. If you settle for $\exists\forall\exists$ instead, you can do away without any form of choice in either the axiom system or metatheory, using only full comprehension. Instead of introducing higher-order functions to simulate $\forall\exists$ quantifier alternations, introduce higher-order predicates for subformulas of the original formula: for example,

$$\forall x_1\,\exists y_1\,\forall x_2\,\exists y_2\,\forall x_3\,\exists y_3\,\phi(x_1,y_1,x_2,y_2,x_3,y_3)$$

is equivalent to

$$\begin{align} \exists P_1,P_2\,\Bigl(&\forall x_1,y_1,x_2,y_2,x_3\,(P_2(x_1,y_1,x_2,y_2)\to\exists y_3\,\phi(x_1,y_1,x_2,y_2,x_3,y_3))\\ {}\land{}&\forall x_1,y_1,x_2\,(P_1(x_1,y_1)\to\exists y_2\,P_2(x_1,y_1,x_2,y_2))\\ {}\land{}&\forall x_1\,\exists y_1\,P_1(x_1,y_1)\Bigr). \end{align}$$

Answer 2

This implies the axiom of choice.

Let $\{A_i\mid i\in I\}$ be a family of non-empty sets, consider the language with predicates $R_i$, for $i\in I$, with the model whose universe is $\bigcup A$ and $R_i=A_i$. Now $\forall R_i\exists x(x\in R_i)$ and the $f$ we have is exactly a choice function from the $A_i$'s.