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 consistentHeyting algebra in simply typed lambda calculusCan 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.
Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?
soft question;type theory;lambda calculus;boolean functions;homotopy type theory
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.