Question

Is there any relationship between Bourbaki's Epsilon Calculus and Lambda Calculus ? Whether $\lambda {x}$ is same as $\tau _{x}$ ? Are the rules of Meta-Mathematics (Criteria of Substitution, Formative Constructions) described in Bourbaki equally applicable to Lambda Calculus ?

Answer 1

Bourbaki's tau-box notation is somewhat insane (e.g., see Adrian Mathias's A Term of Length 4,523,659,424,929), so I'll eventually answer in terms of Hilbert's epsilon-calculus.

But first, the laws of variable binding are identical for all reasonable classical and intuitionistic calculi (matters are a little different for substructural and modal logics, but not in a fundamental way). The basic idea is always the same: certain terms introduce bound variables, and within the scope of the binder (a) you can refer to the introduced variable, and (b) variables of the same name introduced outside of it are shadowed. Furthermore, renaming bound variables does not change the meaning of a term (this is called alpha-equivalence), and when substituting a term for a variable, bound variables need to be renamed in order to avoid capturing the free variables of the substituted term (this is called alpha-conversion).

Frege was the first person to really figure out how variable binding works, and this was a sufficiently important discovery that he is a great logician despite the small matter of the inconsistency of his foundational system. (And I do not mean that ironically: it really is a small matter compared to the magnitude of the achievement of understanding binding.)

The similarity you see comes from the fact that $\forall x.\;A$, $\exists x.\;A$, $\epsilon x.\;A$, and $\lambda x.\;e$ are all binding forms, and must all respect the same laws of variable binding. However, the difference between them is best understood in terms of their different types[*], taking $\iota$ to range over individuals, and $o$ to range over propositions.

$$ \begin{array}{lcl} \forall & : & (\iota \to o) \to o \\ \exists & : & (\iota \to o) \to o \\ \epsilon & : & (\iota \to o) \to \iota \\ \lambda & : & (A \to B) \to (A \Rightarrow B) \\ \end{array} $$

What $\forall$ and $\exists$ do is to take a term of type proposition, that has a free variable of type individual, and construct a proposition from it. $\epsilon$, on the other hand, is a choice operation. It says that if you give it a predicate (i.e., a term of type proposition with a free variable of type individual), it will give you a canonical individual satisfying that proposition. $\lambda$ is syntax for function-abstraction. If you give it a term of type $B$ with a free variable of type $A$, it will give you back a function value transporting $A$s to $B$s.

Now, note that unlike $\forall$, $\exists$, and $\epsilon$, lambda-abstraction works at all types. This is why Church introduced the lambda calculus: he had the idea that you could model variable binding once, with lambda, and then introduce $\forall$, $\exists$, and $\epsilon$ as additional constants in the lambda calculus.

If you really have your heart set on Bourbaki's notation, since it eliminates all variables from the calculus, then I recommend you look at de Bruijn indices instead. The intuition there is also link-based, but it is a radically more efficient representation than Bourbaki's.

[*] I am playing a bit fast and loose here, since the right way to understand these things is really in terms of categorical algebra and structural proof theory: I should be using homs and contexts, but no matter.