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.

Morphisms of...Morphisms? A First Look at Slice Categories

So to basically summarize the pattern that we have been using: we introduced mathematical objects, then some generalized notion of mappings between objects which we called "morphisms". We then collected a bunch of objects and morphisms together such that a bunch of nice properties were true, and we called it a category.

A category "is-a" mathematical object, so we figured out what morphisms between categories were: functors, or mathematical procedures. We then said "Hey, a functor 'is-a' mathematical object, what's a morphism between them?" It turns out it's a natural transformation.

But a morphism is-a mathematical object. So what's a "morphism" between morphisms? Is this a "meaningful" question? (It is, but first some references!)

• Saunders Mac Lane, Categories for the Working Mathematician, Chapter II.6 "Comma Categories"
• The Catsters, Youtube Lecture Series "Slice and Comma Categories", 1, 2

(We hope that the reader can see the pattern here, in category theory we started out with remarkably simple, almost comical, premises. We have objects, and we have morphisms. We group all objects of the same sort together into a category. But we can apply this powerful notion of a morphism to any object, and everything in math "is-a" mathematical object. We can then ask, for each object, what's the morphism of this thing? What's a morphism of this morphism? And so on...)

Category of Objects Under and Over a Specific Object

Now, to discuss morphisms between objects, we need to demand that they are the "same sort" of objects. How to do this? Well, we can demand that the morphisms are from one fixed object or dually they go to one fixed object.

More precisely, let b∈C be a fixed object, we can construct "the category of objects under $b$" denoted by $(b\downarrow\mathbf{C})$. Basically the objects are ordered pairs $\langle f,c\rangle$ consisting of morphisms from $b$ and the target of the morphism, and the morphisms are morphisms of the target $h:\langle f,c\rangle\to\langle f',c'\rangle$...well, this doodle should summarize things nicely:

Composition of morphisms is given by composition of these triangles. More precisely, the composition of the morphisms in the base of the triangle. To be formal, lets give the full definition:

Definition 1. Let C be a category, b∈C be some element. Then a "category of objects under b" consists of

1. (Objects) the collection of ordered pairs ⟨f,c⟩ where $f:b\to{c}$ is a morphism in C, and c∈C is an object;
2. (Morphisms) the morphisms are h: ⟨f,c⟩ → ⟨f',c'⟩

such that the following diagram specifies this

Consider any one point set $*$, and any other set $X$. The function $*\to{X}$ is a single element of $X$. The category of objects under $*$ consist of objects $\langle *\to{X},X\rangle$ which is a selected element of $X$, and the set $X$. This is precisely Set_*, the first part of the ordered pair (the morphism) is the "base point", the second part of the ordered pair is the set itself.

Now, as alluded to earlier, we can reverse the direction of the arrows by "duality". This ends up letting us consider morphisms with the same target.

That is, if we have a category C and an object a∈C, then we can construct a category with the objects being ⟨c,f⟩ where f : c → a is a morphism.

The morphisms in this category would be "morphisms of morphisms". More precisely, it would make the following diagram (on the right) commute:

As we reversed the direction of the arrows, we should probably distinguish this sort of category of objects over a from the category of objects under b. We denote it by (C ↓ a), compared to (b ↓ C) for objects under b.

Formally, this is summarized in the following definition:

Definition 2. Let C be a category, a∈C be some element. Then a "category of objects over a" denoted by (C ↓ a) consists of

1. (Objects) the collection of ordered pairs ⟨f,c⟩ where $f:c\to{a}$ is a morphism in C, and c∈C is an object;
2. (Morphisms) the morphisms are h: ⟨f,c⟩ → ⟨f',c'⟩

such that the following summarizes the category:

Observe that this is just the same as the category of objects under b, except we have the arrows be reversed.

We should consider, to be kosher, what (Set ↓ *) is. The objects are ordered pairs, as before, consisting of ⟨X → *,*⟩ where the first component of the ordered pair is unique. There is always a map in Set from X to a singleton *, it's very boring though -- it's the constant map. It's a unique map too (this is kind of trivial, where else could it map stuff to? There's only one choice!).

The morphisms are really just morphisms between the sets.

Lets think for a second: for each object X∈Set there is a unique object ⟨X → *,*⟩ in (Set ↓ *); and for each morphism f∈hom_Set(X,Y) there is a corresponding morphism in (Set ↓ *).

Since there is a unique one-to-one correspondence between objects and between morphisms in the two categories, we can represent this by a functor which is invertible. What does this mean? It's an isomorphism...i.e. (Set ↓ *) is isomorphic to Set!!!

Remark: Notation

Apparently Mac Lane uses two notations. One is what we've seen. The other is writing C/c for (C ↓ c), and (one assumes) c/C for (c ↓ C). Just be warned there are two different notations (apparently).

[More to follow...apologies to those who would've liked more, duty calls at my job]