Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

Question

I know very little about what I am talking about in what follows, so I appreciate any all help in pointing out all of my mistakes -- otherwise I won't be able to learn more and advance in my knowledge of these interesting subjects.

I want to learn about lambda calculus because it seems like an interesting way to think about functions in general, and because a generalization called the stochastic $\pi$ calculus studied by Luca Cardelli and others seems to allow many computational interpretations of biology, something which I am really interested in. Also other reasons, like wanting to learn and understand functional programming, in order to have an alternative to C++ which I dislike.

However, I just learned that type theory, at least as stated by Lof, is supposed to be a way to formalize intuitionistic logic/constructive mathematics, which rejects the Law of the Excluded Middle and even the Axiom of Choice. My background is more in mathematics than computer science, so although I can see how having to construct something to prove that exists is an acceptable restriction for people interested primarily in computation, I am really uncomfortable with having to give up proof by contradiction and the Law of the Excluded Middle. Perhaps that makes me old-fashioned, and my grandkids will laugh at me for this concern, but proof by contradiction can be very useful and is how I learned a lot of the math which I know.

Is there a way to learn about $\lambda-$calculus and type theory while at least being agnostic about the Law of the Excluded Middle and not outright rejecting it?

The discussion on p.9 of the Homotopy Type Theory book seems to say something to the effect that Univalent Foundations and Homotopy Type Theory can be compatible with the Law of the Excluded Middle and the Axiom of Choice, even though they contradict the univalent axiom? Needless to say I did not quite understand the argument about (-1) types and thus am still somewhat skeptical and unconvinced.

Also, in one of his lectures at the Oregon Programming Language Summer School posted on youtube, Professor Awodey, one of the big names behind the IAS's Homotopy Type Theory/Univalent Foundations Project, seems to identify the Heyting algebra as underlying logic, rather than the Boolean algebra. I read somewhere else (I forgot where unfortunately), that Heyting algebra is what results if one rejects the Law of the Excluded Middle, and thus presumably founding logic upon Boolean algebra means accepting the Law of the Excluded Middle.

Ideally I would prefer to not have to choose between $\lambda$-calculus and Boolean algebra, since the latter underlies most of my understanding of logic, and is also the basis for probability theory, which I know very well and would not like to give up or reject as half-baked. Also I thought Boolean functions were a very hot topic of computer science research, so it seems kind of strange that some computer scientists would prefer Heyting algebra.

These questions might be relevant: Where is the proof that Coq + Excluded Middle is consistent
Heyting algebra in simply typed lambda calculus
Can boolean algebra be expressed in simply typed lambda caclulus?

If they even answer my question, would you mind explaining to me how (as if I were five, so to speak)? I don't quite understand the discussions on them.

Answer 1

You seem to be confusing several things here.

First of all, like Alexis said in her answer, I don't see why you would need to accept/reject the principles of a given logical theory in order to study it and learn about it. The fact that your theory is intuitionistic doesn't mean that your meta-theory has to be! You may freely use proof by contradiction or the axiom of choice in order to prove results about the $\lambda$-calculus (people do that all the time).

Second: you seem to be interested in the $\lambda$-calculus as a programming langage, which means you can safely ignore (at least on a first approach) its connections to intuitionistic logic. You may have heard about the Curry-Howard correspondence and the fact that the $\lambda$-calculus and type theory are deeply connected, which is great, but is not necessarily the preferred route from your point of view. Blurring the distinction between functional programming and proof theory is wonderful but, in your case, it seems to have generated more confusion than anything.

Third: if the stochastic $\pi$-calculus is what you are really interested into, then perhaps you should first look into standard process calculi, starting from CCS (arguably the simplest) and the related machinery (bisimulations, etc.) and then moving on to the $\pi$-calculus. In fact, I think you may even skip the $\lambda$-calculus entirely; at any rate, there is no need to look into intuitionistic logic at all. (Personally, I know some experts of probabilistic concurrency who only have a superficial understanding of the $\lambda$-calculus).

Fourth: if you really are into Curry-Howard, then be reassured that functional programming is not at odds with classical logic: proof by contradiction has a well-known correspondence in programming languages. Googling "computational content of classical logic" should get you started on that. But I wouldn't look into that unless you first make sure you got rid of the confusion you have between the $\lambda$-calculus as a programming language and its relationship with proof theory (that is, until you have understood what Curry-Howard is about), lest you get even more confused.

Answer 2

To me, your question seems analogous to saying "I've heard that non-Euclidean geometry requires me to give up Euclid's fifth axiom, which is very useful in many mathematical contexts." You don't have to give up the axiom in the sense of "personally agree, at a basic philosophical level, that it doesn't hold", you just have to think of it in terms like: "As a thought experiment, what sort of mathematics results if we assume it doesn't necessarily hold?"

Also, you might be interested in these blog posts by Andrej Bauer: "The Law of Excluded Middle" and "Proof of negation and proof by contradiction".

Answer 3

Type theory is a mathematical theory in which we can do very many different things (set theory is like that as well). We can use type theory for computability, or homotopy theory, or use it to express features of a programming language, etc. One of the things that we can use type theory for is as a kind of logic (this is known as Curry-Howard correspondence). When we do logic this way we say that we are doing it internally inside type theory. And then a question arises: what kind of logic is it? Answer: excluded middle is not valid (but neither is its negation) and the axiom of choice is valid.

The reason that everyone brings in logic and excluded middle and all that when they speak about type theory and $\lambda$-calculus is that "everyone" tends to be a bunch of logicians and other people who are interested in foundations of mathematics (myself included). You can learn $\lambda$-calculus completely without any reference to logic by simply learning a functional programming langauge such as Haskell (although they tend to be crazy about category theory). Perhaps OCaml or Scheme is a better choice, those would be the pragmatic descendants of $\lambda$-calculus.

So if we do logic inside type theory using the Curry-Howard correspondence then we find out that it is intuitionistic. But if we do logic somewhere else, for instance in classical set theory, then it is classical. Nobody forces you to believe in One True Logic (although you would certainly get that impression as an undegraduate student of mathematics) so there is nothing to "give up". It is just a matter of fact that you happen to be educated in the tradition of classical logic and so you feel like that's "your true logic". It takes a couple of years to get used to a different logic, but it's doable.

The remarks in the HoTT book that you are referring to are about a different point: if we make a slight technical alteration to the Curry-Howard correspondence (we use $(-1)$-types instead of all types) then we get a different way of doing logic in type theory. This different way says nothing about validity of excluded middle, and nothing about validity of the axiom of choice. So you're free to either accept them or deny them, as you wish (and you have to live with the consequences).

Answer 4

I agree with Alexis and Damiano, and there is another dimension to $\lambda$-calculus that is not often emphasised, because of the dominance of the Curry-Howard correspondence in thinking about the $\lambda$-calculus.

Typed $\lambda$-calculus can be used to represent formulae of classical logic. The most well-known system used for this purpose is the simply typed $\lambda$-calculus (1). It is used as syntax for higher-order logic formulae, a classical logic with excluded middle. Interactive proof assistants based around the LCF-paradigm (4) such as HOL, HOLlight and Isabelle/HOL (2) all do this. This approach is agnostic about what proofs are. The LCF-style thm data-type is one answer.

A related use of typed $\lambda$-calculus for classical logic is in typed logic programming with systems such as $\lambda$Prolog (3).

Finally, and unrelated, if you want to understand the connection between $\lambda$-calculus and $\pi$-calculus, I suggest to study Milner's groundbreaking translation (5) of the former into the latter. It shows that functional computation is a well-behaved from of message passing, thus giving formal meat to intuitions expressed in the 1970s by Carl Hewitt and others.

---

<sub>1. A. Church, A Formulation of the Simple Theory of Types.
2. L. C. Paulson, A Formulation of the Simple Theory of Types (for Isabelle).
3. G. Nadathur, D. Miller, An Overview of Lambda-Prolog.
4. J. Harrison, The LCF Approach to Theorem Proving.
5. R. Milner, Functions as processes.</sub>