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.

A Remark on Reading Bourbaki

A very brief and small remark that may be helpful to those that are studying Bourbaki. The first volume of the Elements of Mathematics (The Theory of Sets) is more or less useless.

The only useful (and in my humble opinion, coherent) parts of that book is the "Summary of Results".

Although, if one were really "hardcore", one would have a collection of e.g. composition notebooks to write notes on the series. By giving actual explanation and examples, it should expand the size of the text several fold.

Also, it helps to create a "cheat sheet" of notation. Bourbaki used bizarre notation since, I assume, they had to work with typewriters.

Unfortunately, no one uses their notation. So, we are forced to come up with a "Rosetta stone" to translate their notation into modern notation.

Some guidelines for your "Rosetta Stone for Bourbaki" might be:

1. Include the book and page numbers where it is first introduced or defined.
2. Include definitions, since those too are "Bourbaki-dependent".
3. Have a separate "Stone" for each book.

I just thought that it may be helpful to someone trying to read through this ancient tome…

Addendum Tuesday August 16, 2011 at 01:10:11PM (PDT)

After some more research, I found out that the bizarre system Bourbaki uses in The Theory of Sets is really something called "Epsilon Calculus."

Math Overflow had a discussion on Bourbaki's epsilon calculus which is useful, and the Stanford Encyclopedia of Philosophy's page is instructive.

I doubt that this system was intended to be fully used, since (as some pointed out in the math overflow discussion) "even trivial proofs require an astonishing number of steps directly from axioms. Existence of the empty set can be proved with 11,225,997 steps and transfinite recursion can be proved with 11,777,866,897,976 steps."

The internet encyclopedia of philosophy states:

The growing awareness of the larger meaning and significance of epsilon calculi has only come in stages. Hilbert and Bernays introduced epsilon terms for several meta-mathematical purposes, as above, but the extended presentation of an epsilon calculus, as a formal logic of interest in its own right, in fact only first appeared in Bourbaki's Elements de Mathematique (although see also Ackermann 1937-8). Bourbaki's epsilon calculus with identity (Bourbaki, 1954, Book 1) is axiomatic, with Modus Ponens as the only primitive inference or derivation rule. Thus, in effect, we get:

(X ∨ X) → X,
X → (X ∨ Y),
(X ∨ Y) → (Y ∨ X),
(X ∨ Y) → ((Z ∨ X) → (Z ∨ Y)),
Fy → FεxFx,
x = y → (Fx ↔ Fy),
(x)(Fx ↔ Gx) → εxFx = εxGx.

This adds to a basis for the propositional calculus an epsilon axiom schema, then Leibniz' Law, and a second epsilon axiom schema, which is a further law of identity. Bourbaki, though, used the Greek letter tau rather than epsilon to form what are now called "epsilon terms"; nevertheless, he defined the quantifiers in terms of his tau symbol in the manner of Hilbert and Bernays, namely:

(∃x)Fx ↔ FεxFx,
(x)Fx ↔ Fεx¬Fx;

and note that, in his system the other usual law of identity, "x = x", is derivable.

The principle purpose Bourbaki found for his system of logic was in his theory of sets, although through that, in the modern manner, it thereby came to be the foundation for the rest of mathematics. Bourbaki's theory of sets discriminates amongst predicates those which determine sets: thus some, but only some, predicates determine sets, i.e. are "collectivisantes". All the main axioms of classical Set Theory are incorporated in his theory, but he does not have an Axiom of Choice as a separate axiom, since its functions are taken over by his tau symbol. The same point holds in Bernays' epsilon version of his set theory (Bernays 1958, Ch VIII).

Source: Internet Encyclopedia of Philosophy.

Over at the nLab, the entry on Choice Operators really helps explain what that pesky τ operator is in Bourbaki's Theory of Sets.