getting rid of existential quantifiers

Question

It seems to me that for most of the twentieth century, axiomatic foundations for mathematical theories were constructed with the (mostly allied) goals of minimizing the number of primitive notions and minimizing the number of axioms. But one could equally well be guided by the goal of minimizing the logical depth of the axioms, i.e., minimizing the use of quantifiers.

Consider group theory, for instance. I have seen formalizations of group theory that say "There exists an element $h \in G$ such that for all $g \in G$, $gh=hg=g$" and then go on to prove that $h$ is unique and to name it $e$. But I have also seen formalizations that say "A group is a set $G$ equipped with an element $e$ such that..." which eliminates the need for a quantifier in an axiom. Likewise, if one includes the operation $g \mapsto g^{-1}$ as a primitive, one can avoid the axiom "For all $g$ there exists $h$ such that $gh=hg=e$" (or worse, "For all $g$ there exists $h$ such that for all $h'$, $ ghh'=hgh'=h'gh=h'hg"$, which I haven't seen, but which I can imagine a certain sorts of purist preferring!).

I know that in constructive mathematics, the status of existential quantifiers is suspect to begin with, so I imagine that there's already quite a bit of writing in foundations and philosophy of mathematics (and maybe computable mathematics as well) that addresses this issue. Some pointers to relevant literature would be appreciated.

Answer 1

You're thinking of the process known as Skolemization, which eliminates existential quantifiers at the cost of introducing new function or constant symbols in the language. The identity and inverse situation you describe are both examples of this.

The process is generally straightforward. To Skolemize the a formula like $$\forall x \exists y (P(x,y) \rightarrow \forall z Q(y,z)),$$ we introduce a new unary function symbol $f$ and we obtain the Skolem normal form $$\forall x (P(x,f(x)) \rightarrow \forall z Q(f(x),z)).$$ Note how the new function depends only on the variable $x$ since the $\exists y$ quantifier we are replacing is not within the scope of the $\forall z$ quantifier.

The Skolem normal form is always equisatisfiable with the original: if the first has a model then the second has a model and vice versa. In fact any model of the original sentence can be expanded to a model of the new sentence by interpreting the new symbols functions that pick appropriate witnesses for the statements involved. (This construction requires the Axiom of Choice to carry out in full generality.)

One drawback of Skolemization is that the new functions can be very complex and thus models become harder to describe. For example, it is often the case that the original sentence has a computable model but that the Skolem normal form does not. Another drawback is that function symbols are sometimes undesirable or unnatural. For example, the usual density axiom for linear orders $$\forall x \forall y(x \lt y \rightarrow \exists z(x \lt z \land z \lt y))$$ is rarely seen in its Skolemized form $$\forall x \forall y(x \lt y \rightarrow x \lt b(x,y) \land b(x,y) \lt y)$$ since one usually thinks of linear orders as strictly relational structures.

Answer 2

The classical approach to defining quantifier complexity classes is syntactic. For example, a $\Sigma_2$-formula starts with an existential quantifier followed by an universal one and then by an unquantified kernel; and vice versa for a $\Pi_2$-formula. The quantifier complexity concept usually becomes more robust if some form of bounded quantifiers (like $\exists x < y$ or maybe $\exists x\in y$, depending on the language of the theory) is allowed in the unquantified kernel.

A deeper insight into the complexity of axioms, predicates, functions... can be obtained by only requiring equivalence with a formula of such a form (this is especially natural when defining classes such as $\Delta_i$ which are supposedly those formulae, predicates, functions... that can be expressed in both the $\Sigma_i$ and $\Pi_i$ form). The question then is, equivalent in which theory; the specific formulation of other axioms (rather just the language of the theory) starts to matter. Furthermore, it does not makes much sense to evaluate the complexity of an axiom within a theory it is itself included in, because it is then generally equivalent to any simplest theorem like $0=0$ or $(\exists x) x=x$ of that theory.

There is a substantial amount of research on both generally applicable techniques such as Skolemization described in a sister answer and its Herbrandization counterpart and also on quantifier complexity in the context of various theories.

For example, in the context of set theory the hierarchy of quantifier complexity of formulae is called Lévy hierarchy and quite widely studied to this day.

Probably the best example of the impact of quantifier complexity on a mathematical field I am aware of is the computability theory, particularly its Arithmetical hierarchy.

There is also a field of computational complexity that succeeded in deriving interesting correspondences between the polynomial hierarchy (comprised of the most popular computational complexity classes such as $P$, $NP$,...) and so-called bounded quantifier complexity which measures quantifier complexity of arithmetical formulae differently than usual. Bounded quantifiers are counted, and an even weaker form of bounded quantifiers (quantifiers bounded by a logarithm of something else) are allowed for free. An overview of the field is in this monograph.

Answer 3

In classical logic, there is a natural symmetry (or duality) between the universal and the existential quantifier, and each one can be expressed in terms of the other. (Similar to the duality between $\vee$ and $\wedge$ in classical propositional logic.)

Classical logic and constructive mathematics interpret the universal quantifier in the same way, but they differ on what the existential quantifier means. An intuitionist or constructivist will only claim $A\vee B$ ($\exists x:A(x)$, respectively) if he knows that $A$ holds, or knows that $B$ holds (if he knows an $x$ for which $A(x)$ holds, respectively).

But this asymmetry between $\forall $ and $\exists$ also appears in textbooks based on classical logic. Assumptions such as "There exists $x$ with $\forall y( y+x=y) $" are almost always "skolemized"; this means that a new constant symbol $0$ and a new axiom $ \forall y (y+0=y)$ is introduced. It is a basic fact of logic that skolemization is "allowed" (technical term: leads to a conservative extension).

Similarly, a sentence "forall $\delta$ there is an $\varepsilon$ such that $A(\delta, \varepsilon)$" is often reformulated in a skolemized form as "[there is a function $\epsilon(\cdot)$ such that] for all $\delta$ we have $A(\delta, \epsilon(\delta))$".

I do not know any references, but in my opinion there are several reasons:

1. historically, the notion of a function $\epsilon(\cdot)$ (or a constant $0$) .has been around for much longer than the concept of an existential quantifier.

2. [EDIT] Related: you can plug constants and functions into functions; e.g., from $A(c)$ and $\forall x: B(x, f(x))$ most formal proof systems will trivially derive $A(c) \wedge B(c,f(c))$. Depending on your system, it may not be so trivial to get from $\exists x: A(x)$ and $\forall x\, \exists y: B(x,y)$ to $\exists x\, \exists y: A(x)\wedge B(x,y)$

3. (arguably,) from a didactical as well as the linguistic point of view it is easier to talk about $0$ and $\epsilon(\delta)$ rather than "the/some element satisfying $\cdots$" or "some $\varepsilon$ which by our assumption on continuity must exist". (This is in particular true if there is a unique or canonical object $0$ or $\epsilon(\delta)$.)

4. Skolemized sentences have fewer quantfiers, so they are easier to understand

5. Dependencies between variables become clearer. Also, skolemization is the most convenient form to express Henkin quantifiers ("for all $x,y$ there exists $p$, $q$ such that $\cdots$, but $p$ depends only on $x$, and $q$ only on $y$").

6. Even though most mathematicians base their arguments (often subconsciously) on classical logic, they still have a feeling for what a "constructive" proof is, and they will prefer a constructive proof over a nonconstructive one. Skolemization allows one to keep track of the non-computable or non-constructive steps in an argument. (E.g.: "For every $k$ there is an $N=N(k)$ such that for all $m>N(k)$ $foo(m,k)$ holds --- here, $N(k)$ can/cannot be directly computed from $k$.")

Answer 4

Hilbert's epsilon-calculus is another method to completely get rid of all existential quantifiers as well as all universal quantifiers. It is almost, but not quite, entirely unlike Skolemization.

For any formula $A(x)$, the term $\epsilon x(A(x))$ is read as "any $x$ satisfying property $A$, if there is any -- and anything else otherwise". Thus the formula $A( \,\epsilon x(A(x))$ says that $A$ holds for such an $x$, i.e., $\exists x\, A(x)$ holds. The formula $\lnot A( \ \epsilon x(A(x) \ )$ then says that $A$ does not even hold for the $x$ which, if at all possible, satisfies $A$, or in other words: $\lnot \exists x(A(x))$.

The universal formula $\forall x (B(x))$ can therefore be rewritten as $B(\ \epsilon x (\lnot B(x))\ )$. ("Pick some $x$, any $x$ -- if there is one at all -- which fails property $B$. Then $B$ will hold even of this $x$. So you failed to pick a counterexample. So $B$ holds for all $x$.")

Theoretically this is wonderful -- not need for quantifiers, and you can use $\epsilon$ like a real term, you can plug terms into terms, etc. In practice it did not catch on at all -- probably because formulas get very complicated very quickly, and also because the "meaning" of $\forall x (B(x))$ is so much easier to understand than the meaning of $B(\ \epsilon x (\lnot B(x))\ )$.

Answer 5

There is some interesting stuff about this in Johnstone's book on Stone Spaces. In particular, he discusses what he calls "cartesian theories". Such a theory has a list of axioms, and if axiom $n$ says that there exists $x$ with property $P$, then axioms $1$ to $n-1$ imply that that $x$ is unique. He has some examples where natural non-cartesian theories are equivalent to less obvious cartesian theories, and other examples where this is not possible. It is familiar that purely equational theories can be interpreted in any category with finite products. I think it works out that cartesian theories can be interpreted in any category with finite limits.

It is also interesting to look at software systems like Isabelle, Coq and Agda that can check suitably formalised proofs. I am most familiar with Agda, which has strongly constructive foundations. In Agda it is difficult and unnatural to formulate a bare existence statement; you could say that existential quantifiers are skolemized by default.