Epsilon Calculus

So, this is a post consisting of notes for myself on Hilbert's ε-calculus...specifically with regards to Bourbaki's use of it.

What is ε Calculus?

We work with first order languages. So, we have predicates, terms, etc.

Let A be a predicate. Then we interpret εx A as "some x that satisfies A".

We could look at it as returning a term t which satisfies A, or if no such term exists it just returns any term for which A is false.

This seems like a pain to program up, since "return any term which satisfies such-and-such, non-deterministically" is...weird!

How did Bourbaki use it?

Well, formally, Bourbaki used a slightly different notation, and the Internet Encylopedia of Philosophy notes [utm.edu] that "Bourbaki's epsilon calculus with identity (Bourbaki, 1954, Book 1) is axiomatic, with Modus Ponens as the only primitive inference or derivation rule."

This reminds me of the simple propositional calculus Mendelson introduces in chapter 1 of Introduction to Mathematical Logic (fourth ed.). If you are unfamiliar with it, wikipedia [wikipedia.org] has a review of the system. It has one rule of inference (modus ponens) and 3 axioms.

Effectively, the ε operator acts as a choice operator, which means that the set theory framework set up by Bourbaki automatically has the axiom of choice induced by this ε operator.

Moreover, this is a global choice operator, so Bourbaki's axioms are equivalent to something like Zermelo set theory + Axiom of Global Choice.

Aside: Bourbaki Set Theory

I want to discuss in some detail the axioms of Bourbaki's set theory...because it is not ever discussed anywhere.

There is (II §1.4, pg 67 of Theory of Sets) the first axiom, "the axiom of extent":

A1. (∀ x)(∀ y)((x⊂y and y⊂x) implies (x=y)).

This is the axiom of extensionality we all know and love that defines set equality as "two sets are equal if and only if they have the same elements".

The next axiom is what we would call the axiom of pairing, and Bourbaki calls it the "the axiom of the set of two elements" (Theory of Sets §1.5, pg 69):

A2. (∀ x)(∀ y) Coll_z(z=x or z=y)

"This axiom says that if x and y are objects, then there is a set whose only elements are x and y" (Theory of Sets II §1.5, pg 69).

In modern set theory, this is the axiom of pairing which says for all x and y there exists a z such that z={x,y}. This is a little bit sloppy, but that's the content of the axiom.

Next, we have the axiom of the ordered pair (Theory of Sets II §2.1, pg 72):

(∀ x)(∀ x')(∀ y) (∀ y') (((x,y) = (x',y')) implies (x=x' and y=y'))

Nothing controversial here, just the definition of an ordered pair.

There are two axioms left. There is the axiom of the set of subsets (Theory of Sets II §5.1, pg 101):

(∀ X) Coll_Y (Y⊂X)

This amounts to specifying that the power set of any set X exists.

Now the last axiom for Bourbaki's set theory is the axiom of infinity (Theory of Sets III §6.1, pg 183):

A5. There exists an infinite set.

That's it! That's everything! As homework exercise, prove it's formally equivalent to Zermelo's axioms...

Now, what about the axiom of choice? Well, actually, Bourbaki has it covered:

Theorem 1 (Zermelo). Every set E may be well-ordered.

The proof (pp. 153--54) uses, yep you guessed it, the ε choice operator. Basically, take the power set, then throw away the element E in the power set. For each element in this collection of proper subsets, choose an element using ε-calculus.

This induces an ordering of elements because the power set is a complete lattice (with respect to the ordering given by inclusion). Thus we obtain an ordering on the set, and it follows any (nonempty?) set can be well-ordered.

This is equivalent to the axiom of choice. If we allow the scheme of ε extensionality:

∀x ((A(x) if and only if B(x)) implies (εx A = εx B))

What happens? As a consequence to this, we get the Axiom of Global Choice [wikipedia.org].

In Automated Theorem Proving

Martin Giese , Wolfgang Ahrendt's "Hilbert's epsilon-Terms in Automated Theorem Proving" (eprint [citeseerx.ist.psu.edu]) discusses the role the epsilon calculus has had in automated theorem proving.