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.

Proclus on Euclid

Proclus wrote some commentaries on Euclid's Elements and found a pattern to the presentation of material:

Every Problem and every Theorem that is furnished with all its parts should contain the following elements: an enunciation, an exposition, a specification, a construction, a proof, and a conclusion. Of these enunciation states what is given and what is being sought from it, a perfect enunciation consists of both these parts. The exposition takes separately what is given and prepares it in advance for use in the investigation. The specification takes separately the thing that is sought and makes clear precisely what it is. The construction adds what is lacking in the given for finding what is sought. The proof draws the proposed inference by reasoning scientifically from the propositions that have been admitted. The conclusion reverts to the enunciation, confirming what has been proved.

Lincoln used this approach in his rhetoric, as Hirsch & Van Haften notes in their book Abraham Lincoln and the Structure of Reason. In an interview, they explained each step.

For the enunciation, think in terms of: Why are we here. It contains short, indisputable facts. They are part of the given. It also includes a sought. This is a high level statement of the general issue being discussed.

For the exposition, think in terms of: What do we need to know relating to what is given. These are additional facts, generally fairly simple, and indisputable. These facts take what was in the enunciation’s given, and prepare for use in the investigation (in the construction).

For the specification, think: What are we trying to prove. The specification is a more direct restatement of the enunciation’s sought. While the sought is frequently neutrally stated, the specification is a direct statement of the proposition to be proved.

For the construction, think: How do the facts lead to what is sought. The construction adds what is lacking in the given for finding what is sought.

For the proof, think in terms of: How does the admitted truth confirm the proposed inference. The proof draws the proposed inference by reasoning scientifically from the propositions that have been admitted.

For the conclusion, think: What has been proved. The conclusion reverts back to the enunciation confirming what has been proved. The conclusion should be straightforward, forceful, and generally short.

It might be useful if anyone ever goes into mathematics...or Law...

Addendum: Modern Mathematics

It seems that this format can be used in modern mathematics. Andrei Rodin's "Doing and Showing" (arXiv:1109.4298 [math.HO]) notes on page 25 how a modern theorem/proof can be formulated in the Euclidean tradition:

Theorem 3:
Any closed subset of a compact space is compact

Proof:
Let F be a closed subset of compact space T and {F_α} be an arbitrary centered system of closed subsets of subspace F ⊂ T. Then every F_α is also closed in T, and hence {F_α} is a centered system of closed sets in T. Therefore ∩F_α = ∅. By Theorem 1 it follows that F is compact.

Although the above theorem is presented in the usual for today's mathematics form "proposition-proof", its Euclidean structure can be made explicit without re-interpretations and paraphrasing:

[enunciation:]
Any closed subset of a compact space is compact

[exposition:]
Let F be a closed subset of compact space T

[specification: absent].

[construction:]
[Let] {F_α} [be] an arbitrary centered system of closed subsets of subspace F ⊂ T.

[proof :] [E]very F_α is also closed in T, and hence {F_α} is a centered system of closed sets in T. Therefore ∩F_α=∅. By Theorem 1 it follows that F is compact.

[conclusion: absent ].

The absent specification can be formulated as follows:

"I say that F is a compact space"

while the absent conclusion is supposed to be a literal repetition of the enunciation of this theorem.

Role of Examples

I have noticed authors use examples in math texts in two ways: demonstrating how to perform an algorithm, or silently giving an exercise to the reader.

An instance of the "demonstration" type example would be found in any calculus textbook that goes through a calculation step-by-step detailing what is happening, etc.

The "exercise" type of example is found in most upper division and graduate texts. It gives enough information to say "Well, this gadget is an example of a group/ring/field/measure/space/etc." but fails to prove it.

So which type of example is appropriate for mathematical writing?

Well, it depends on the writing. I'm writing so I can remind myself of some field or concept, so I can learn it all over again in 5 minutes.

With this sort of writing, the "demonstrations" are more appropriate.

However, in monographs the latter seems conventional. Regarding monographs I'd like to quote Serge Lang:

I have not written this course in the style I would use for an advanced monograph, on sophisticated topics. One writes an advanced monograph for oneself, because one wants to give permanent form to one's vision of some beautiful part of mathematics, not otherwise accessible, somewhat in the manner of a composer setting down his symphony in musical notation. [Emphasis added]

From the Preface to A First Course in Calculus by Lang.

Maybe there is a happy medium, I don't know...

Index Cards

I have been using index cards when studying math, at least now.

It's really useful to write down definitions and theorems on one side (one definition/theorem per card) and explanations of why it's useful on the other side (possibly sketching the proof).

It's been really useful while reading through Kirillov's Lectures on tensor categories and modular functor (eprint [math.sunysb.edu]).

Gel'fand's Generalized Functions reads like a dinner table conversation between mathematicians, without formal definitions in the grocery-list Bourbakist manner. Index cards help out a lot here, enabling you to write down where references are (which was, coincidentally, why they were invented in the first place!).

It's also wonderful when you begin to write a book, you can just collate the index cards of theorems and definitions. Then writing is just a matter of inserting literary "glue" between already existing material.

One can form a wiki [http://takingnotenow.blogspot.com] using index cards.

But instead I prefer to organize notes [studygs.net] slightly differently. It also enables me to "automatically" cite by keeping track of the source in the upper right corner, and label it as a definition or a theorem in the upper left corner.

Plus I am not married to any collation in this scheme. On the other hand, I have to look through all my notes to get to various definitions --- there is no organization to it!

Just more stuff to ponder...

Bourbaki and Sets

Don't worry too much about Bourbaki and Set Theory...Bourbaki didn't really use first order logic, anyways.

At any rate, there was an excellent discussion of the formalism discussed in Bourbaki's Theory of Sets over at the nForum a while back (I don't know how I missed it!).

Someone noted that Bourbaki's set theory is "equivalent" to ZGC (Zarmelo with the Axiom of Global Choice).

Addendum: for more details on Bourbaki's set theory, see the entry on Hilbert's Epsilon Calculus.

Wikipedia claims that Zarmelo set theory is "strong enough to carry out almost all ordinary mathematics not directly connected with set theory or logic" (Wikipedia).

Although, it should be noted, later editions of Bourbaki included the axiom of replacement...making it resemble ZFC more than ZGC (The Bourbaki View, fn 15).

Implications for Automated Theorem Provers

I got my hands ahold of a wonderful book:

• John Harrison, Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009).

Why is it so wonderful? Well, in chapter 6 it discusses Mizar-like declarative proof systems. In fact, the code accompanying the book actually implements a simplified version of it.

It wouldn't be terribly difficult to change the wording to use the Mathematical Vernacular.

Additionally, since the programming language is OCaml, one could take advantage of Camlp4 to extend the grammar to make the syntax prettier.

But I digress.

If one were to implement mathematics formally, one couldn't use ZGC without having problems covering topology (or category theory — large categories are defined how?).

However, if one were to take the conservative extension to ZFC, one would still run into problems (again, large categories?). What one would have to do is use BNG Set Theory.

So for any budding cyber-Bourbaki groups out there: you can't use ZGC, ZFC, but you must use BNG (which is not too bad!).

Although, the more I think about it, the more it doesn't matter as long as the behaviour of sets are "sufficiently nice". The implementation details don't matter for, e.g., the ordered pair...just the fact that (x,y)=(a,b) if and only if x=a and y=b. But now I'm just rambling!

Aside on Axioms and Specifications

One thing I always wondered about: why not use naive specifications instead of constructions (e.g., the ordered pair (x,y) as {{x,∅},{y}} or a million other different ways) or rigid axioms?

The answer is that a specification is axiomatic. One specifies the axiomatic behaviour through specifications, it would be logically equivalent to giving an axiomatic framework.

Addendum

To any budding cyber-Bourbakites out there, you will be relieved to find out that there exists an automated proof checker, the "Zermelo Proof Checker", which is based on the BNG axioms for set theory and some minor type theory.

If, like me, you use older hardware...you will run into problems when using zprover. Namely, eprover will always time out, saying something like "CPU time limit exceeded".

Well, zprover is a script that calls eprover and has a parameter that can be (and should be) changed on line 10:

TIME_LIMIT=5 # in seconds

Change it to 60, or something greater.