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 ?
$\begingroup$
$\endgroup$
3
-
4$\begingroup$ They certainly aren't the same: $\lambda x$ applies to terms whereas $\tau_x$ applies to formulas. So $\lambda x.x$ is the identity map, but $\tau_x x$ makes no sense since $x$ is not a well-formed formula. Similarly $\lambda x.(x = x)$ makes no sense, but $\tau_x (x=x)$ is a choice of element of the universe. (You could view equality as a binary function that takes values in a truth-value sort, but then $\lambda x.(x = x)$ is the same as $x=x$ not an element of the sort of $x$.) $\endgroup$– François G. DoraisCommented Jan 23, 2012 at 12:07
-
1$\begingroup$ I think I should have used more precise language. What I meant, whether Lambda Calculus and Bourbaki's Epsilon Calculus have similarity ? I did not mean to assert that $x$ in $\lambda{x}$ and $x$ in $\tau_{x}$ are same. Is not rules of quantification as illustrated in Quine, rules of Meta-Mathematics as in Bourbaki and Lambda Calculus share same theme ? $\endgroup$– nature1729Commented Jan 23, 2012 at 12:58
-
$\begingroup$ As to whether lambda and epsilon "have similarity", the only similarity that I see is that they both bind a variable. So Neel's answer pretty much covers what there is to say. $\endgroup$– Andreas BlassCommented May 4, 2016 at 20:27
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
answered Feb 7, 2012 at 15:34
-
2$\begingroup$ +1, Neel. This is a really well thought-out reply. $\endgroup$ Commented Feb 7, 2012 at 15:49