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?

  • 1
    $\begingroup$ Isn't this obviously a choice principle? The function $f$ is making choices for you, choosing for each $x$ a particular witness $y$, namely $y=f(x)$, among all the possible witnesses $y$ that could work. It seems like the very essence of choice, and any instance of choice could be converted into such a case. $\endgroup$ Dec 18 '14 at 3:40
  • $\begingroup$ I don't know that it's obviously full choice and not something weaker like countable choice, since first order theories have countable models. As someone who is a not a mathematician, choice always being required for any Skolemization is acceptable as an answer, but I find it a bit surprising given how readily I use Skolemization for my proof calculus. $\endgroup$
    – dezakin
    Dec 18 '14 at 4:02
  • 1
    $\begingroup$ It might be worth stressing that the usual Skolem theorem for first-order logic (i.e., that the skolemization of a theory is its conservative extension) does not require any choice, or even set theory for that matter (it can be formalized in a weak fragment of arithmetic). $\endgroup$ Dec 18 '14 at 12:13
  • 1
    $\begingroup$ Right. This is a nice example showing how the completeness theorem fails in absence of the BPIT. $\endgroup$ Dec 18 '14 at 13:50
  • 3
    $\begingroup$ By referring to the statement $(\forall x\exists y\,\phi(x,y))\iff(\exists f\forall x\,\phi(x,f(x))$ as an identity, the OP probably meant that this statement should be valid, i.e., true in all structures. If that was the intention, then, as Joel said, the full axiom of choice is required. $\endgroup$ Dec 18 '14 at 17:24

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}$$

  • $\begingroup$ Everyone knows that second-order logic is set theory in sheep clothing. "Bahhh... baahhhh..." $\endgroup$
    – Asaf Karagila
    Dec 18 '14 at 14:31
  • $\begingroup$ Does this mean using Henkin semantics doesn't require choice then, because first order theories don't require choice for Skolemization and Henkin semantics essentially makes higher order theories multi-sorted first order theories? $\endgroup$
    – dezakin
    Dec 18 '14 at 21:18
  • 1
    $\begingroup$ I’m not sure this is the right way to think about it. First, usual skolemization in one-sorted first-order theories still has a different meaning than the kind of skolemization you consider in the higher-order (multi-sorted first-order) theories: the former is a metamathematical closure property of the logic (a form of an admissible rule), whereas the latter is an actual formula (or schema) in the logic. It’s also problematic to involve semantics in the issue, since just like for plain first-order logic, the completeness and compactness of Henkin semantics (for uncountable languages) ... $\endgroup$ Dec 19 '14 at 16:38
  • 1
    $\begingroup$ ... requires a weak (actually, not so weak) form of choice, namely the Boolean prime ideal theorem. But having said that, the choice schema $(*)$ may be true in a Henkin-style model even if the axiom of choice fails for sequences of subsets of the model, because the validity of the schema only concerns sequences of sets uniformly definable in the model by a formula. $\endgroup$ Dec 19 '14 at 16:43

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.

  • 3
    $\begingroup$ It's even equivalent to choice. $\endgroup$ Dec 18 '14 at 7:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.