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?

Answer 2

I don't know whether this will be helpful, but here goes. There used to be things called the "Laws of Thought", and they used to be equated (tendentiously) with sort-of axioms for rationality, when "axiom" still meant self-evident. After Leibniz there were four basic Laws of Thought, of which you have referenced two.

Now, someone should probably write a book about the subsequent fate of these Laws, but for a mathematical analogy, look at another similar thing, the Principle of Continuity. This was big in the eighteenth century, was questioned in the nineteenth century, and eventually dissolved at the hands of Weierstrass into the epsilon-delta proof technique, i.e. the standard approach of mathematical analysis.

Excluded middle underwent a somewhat parallel development, though it is not as if this is taught as mainstream mathematics. The intuitionists objected to it: basically from a constructive point of view, proof by case analysis is not good unless there is a computable criterion for which case you are in, and excluded middle is what happens with two cases. When intuitionistic logic was written down as a formal system (not the first idea of Brouwer), the structure of propositions came out as a Heyting algebra, not a Boolean algebra.

When the logic of topos theory was recognised to be intuitionistic (not the first idea of Grothendieck!) a bit more could be said. The truth-values (more accurately the subobject classifier) would be a Heyting algebra. The case of "classical logic" of "classical set theory" would be the truth values being the Boolean algebra with two elements. Usually the subobject classifier would be something much more complicated. (As has been pointed out, the "law of non-contradiction" or first Law of Thought is about the truth values not being reduced to just one, which is not the same thing as various other statements.) The result, over all, including the Axiom of Choice because topos theory is a type of set theory not just a propositional logic, is a very sophisticated range of models. "Classical logic" is seen as a very particular form of intuitionistic logic. If the question is about how disjunction actually works in a topos, or how negation works in intuitionistic logic, there are answers: the technicalities will dispel any "mysteries". But it's not au revoir at all: excluded middle is an option and one can say exactly how it fits in.

Answer 3

In a topos, the question is not whether a sentence is true or false, but where it is true, because toposes--at least the geometric ones you're talking about--are generalized spaces. There can be limit points where this question cannot be decided for all sentences. The problem is then that there are other points within any distance (more accurately: any open neighborhood) both where a sentence is true and where the same sentence is false.

Answer 4

A version of Russell's paradox provides a failure of "law of excluded middle". I don't know if this directly answers your question, but it illustrates the constraints on getting this "law" to work.

Define a "logical function" to be one that returns 'yes' or 'no' when given an input. "law of excluded middle" asserts that if the 'yes' inputs are specified then assigning 'no' to everything else defines a logical function. Consider

$R[f]$:= If( $f$ is a logical function) then not($f[f]$), else 'no')

But $R$ cannot be a logical function, for if it were we would have $R[R]= not(R[R]$. The error must be that "($f$ is a logical function)" is not a logical function. If it is not 'true' then it is 'wrong' in the sense that the reasoning is invalid. Usually this is seen as invalidating "unlimited comprehension" (naive set theory).

Most mathematics requires excluded-middle arguments, so we interpret this problem as showing inputs have to be restricted for these arguments to work. In a sense the job of set theory is to provide safe contexts for excluded-middle arguments. This also suggests why set theory is complicated: we cannot describe "safe contexts" using logical functions.