[Math] Au revoir, law of excluded middle

Question

In what way and with what utility is the law of excluded middle usually disposed of in intuitionistic type theory and its descendants? I am thinking here of topos theory and its ilk, namely synthetic differential geometry and the use of topoi in algebraic geometry (this is a more palatable restructuring, perhaps), where free use of these "¬⊨P∨¬P" theories is necessarily everywhere–freely utilized at every turn, one might say. But why and how are such theories first formulated, and what do they look like in the purely logical sense?

You will have to forgive me; I began as a student in philosophy (not even that of mathematics), and the law of excluded middle is something that was imbibed with my mother's milk, as it were. This is more of a philosophical issue than a mathematical one, but being the renaissance guys/gals that you all are, I thought that perhaps this could generate some fruitful discussion.

Answer 1

You make a couple of basic mistakes in your question. Perhaps you should correct them and ask again because I am not entirely sure what it is you are asking:

1. Topos theory does not "freely use $P \lor \lnot P$", and neither does synthetic differential geometry. In fact, topos theorists are quite careful about not using the law of excluded middle, while synthetic differential geometry proves the negation of the law of excluded middle.

2. As far as I know, the law of excluded middle is $P \lor \lnot P$, while the law of non-contradiction is $\lnot (P \land \lnot P)$. These two are not equivalent (unless you already believe in the law of excluded middle, in which case the whole discussion is trivial). The principle of non-contradiction is of course intuitionistically valid. So you seem to be confusing two different logical principles.

If I had to guess what you asked, I would say you are wondering why anyone in their right mind would want to be agnostic about the law of excluded middle (intuitionistic logic) or even deny it (synthetic differential geometry). Aren't people who do so just plain crazy?

To understand why someone might work without the law of excluded middle, the best thing is to study their theories. Probably you cannot afford to devote several years of your life to the study of topos theory. For an executive summary of synthetic differential geometry and its interplay with logic I recommend John Bell's texts on synthetic differential geometry, such as this one.

Let me try an analogy. Imagine a mathematician who studies commutative groups and has never heard of the non-commutative ones. One day he meets another mathematician who shows him non-commutative groups. How will the first mathematician react? I imagine he will go through all the usual phases:

1. Denial: these are not groups!
2. Anger: why are you destroying my groups? I hate you!
3. Bargaining: can we at least analyze non-commutative group in terms of their "commutative representations" (whatever that would mean)?
4. Depression: this is hopeless, I wasted my life studying the wrong groups. I might as well study point-set topology.
5. Acceptance: it's kind of cool that the symmetries of a cube form a group.

I am at stage 5 with regards to intuitionistic logic. Where are you?