$\exists x ~ \forall y ~ f(x, y) \iff \forall y() ~ \exists x~ f(x, y(x))$ Name? Proof?

Question

I was looking at potential theorems, and this one came up:

$$\bigg(\exists x ~ \forall y ~:~ f(x, y) \bigg) \iff \bigg(\forall y() ~ \exists x ~:~ f(x, y(x))\bigg)$$

(where the second $y$ is being quantified over all total unary functions)

Does this proposition have a name? It is a generalization of

$$(a_{00} \land a_{01}) \lor (a_{10} \land a_{11}) \iff (a_{00} \lor a_{10}) \land (a_{00} \lor a_{11}) \land (a_{01} \lor a_{10}) \land (a_{01} \lor a_{11})$$

I'm not even sure which higher order axioms I would use to prove it. Any references or suggestions for proofs or criticisms of the theorem are welcome.

Answer 1

Consider the dual statement: $$ \forall x \exists y\, R(x,y) \iff \exists f \forall x\, R(x, f(x)). $$ (I've used more typical variables in stating it; no good purpose is served by using "$y$" as a variable for two different sorts of things.) This is essentially the Axiom of Choice (AC), and is provable using AC. $f$ is called a uniformizing function for $R$. If further constraints are placed on $R$ and $f$ (such as, "$R, f$ are $\Pi^1_1$", or "$R, f$ are projective"), it may or may not hold in a theory (and may or may not be provable even in ZFC). See the wikipedia article on uniformization for more.

Answer 2

The dual of this (particularly in the context of automated theorem-proving), which results in a $\exists\forall$ formula is called Skolemization or conversion to Skolem Normal form. As pointed out in a comment, the formulation as in the question that leads to $\forall\exists$ formula is often called Herbrandization.

I find Skolemisation more intuitive than Herbrandization: in Skolemisation, you are looking at a string of quantifiers and analysing the dependencies of possible witnesses for the existentially quantified variables. E.g., given, $\forall a\forall b\exists c \forall d \exists e P(a, b, c, d, e)$, $c$ may depend on $a$ and $b$ while $e$ may depend on $a$, $b$, $c$ and $d$. Expressing the existentially quantified variables as functions of the values on which they may depend allows you to move the existentials to the front, turning

$$\forall a\forall b\exists c \forall d \exists e P(a, b, c, d, e) $$

into

$$\exists c\exists d\forall a\forall b\forall c P(a, b, c(a, b), d, e(a, b, c(a, b))).$$

These are equivalent in higher-order logic given the axiom of choice.

Answer 3

The transformation $$ (\exists x)(\forall y) \phi(x,y) \Longrightarrow (\forall f)(\exists x)\phi(x, f(x)) $$ is a special case of a process called Herbrandization. This is dual to the more well known operation of Skolemization. Indeed, if you know what Skolemization is then Herbrandization can be defined as the negation of the Skolemization of the negation of the prenex form a formula:

• Original in prenex form: $( \exists x)(\forall y) \phi(x,y) $
• Negation: $(\forall x)(\exists y)\lnot \phi(x,y)$
• Skolemization of negation: $(\exists f)(\forall x) \lnot \phi(x, f(x))$, or $(\forall x)\lnot \phi(x, f(x))$ if we drop the function quantifier.
• Herbrandization (negation of previous): $(\forall f)(\exists x)\phi(x, f(x))$ or $(\exists x)\phi(x,f(x))$ if we drop the function quantifier.

The Skolemization of a formula may not be equivalent to the original formula, in general, and the same holds for Herbrandization. In general, Skolemization preserves satisfiability, and Herbrandization preserves validity. Precisely: if we drop the quantifier on the function $f$ and instead make it a new symbol in the language, the original formula is valid if and only if its Herbrandization is valid, while the original formula is satisfiable if and only if its Skolemization is satisfiable. In this way we can reduce the question of satisfiability of arbitrary formulas to the question of satisfiability of purely universal prenex formulas, and the question of validity to the question of validity for purely existential prenex formulas.

Herbrandization is a key method in Herbrand's theorem. Also see this answer on MathOverflow.