11
$\begingroup$

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.

$\endgroup$
  • 30
    $\begingroup$ ^wow, the above comment seems a tad acerbic, methinks. $\endgroup$ – lambdafunctor May 20 '10 at 13:57
  • 3
    $\begingroup$ Oh, and I suppose that I didn't realize that topoi weren't relevant to algebro-geometric constructions since Grothendieck. And don't assume that I haven't studied anything about functorial structures in algebraic geometry. $\endgroup$ – lambdafunctor May 20 '10 at 14:00
  • 1
    $\begingroup$ I believe that you know what you're talking about, but also that talking about Grothendieck topoi as though they were elementary topoi is missing the point. $\endgroup$ – Harry Gindi May 20 '10 at 14:20
  • 2
    $\begingroup$ Also, Grothendieck topoi are also examples of elementary topoi (obviously, the converse is NOT generally true), which exist in the universe of intuitionistic type theory--I would refer you to Mac Lane/Moerdijk and Johnstone for an elaboration here. $\endgroup$ – lambdafunctor May 20 '10 at 14:21
  • 3
    $\begingroup$ ^good call. I'll post such an inquiry in a bit. Thanks for the input; it's appreciated. $\endgroup$ – lambdafunctor May 20 '10 at 14:43
77
$\begingroup$

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?

$\endgroup$
  • 11
    $\begingroup$ Why can't I +2 a post... $\endgroup$ – darij grinberg May 20 '10 at 16:24
  • 8
    $\begingroup$ Some people seem to get hung up over whether or not LEM is true. A better question is "what interesting things can I do with or without it?". There is a lot of interesting stuff you get from not using LEM, even if you believe LEM is true. Take that attitude and you can jump straight to stage 5. $\endgroup$ – Dan Piponi May 20 '10 at 19:03
  • 30
    $\begingroup$ There seems to be a stage beyond 5, which we might call "Stockholm Syndrome", where you identify so completely with the new, frightening, more complex world that the enemy of complexity, the original simplicity, becomes your enemy: the only interesting groups are noncommutative, the only valid intuitions about formalisms are constructively well-grounded ones. We've all met stage-sixers, haven't we? $\endgroup$ – Charles Stewart May 21 '10 at 10:27
  • 1
    $\begingroup$ @Charles: I agree with the danger you're describing - obsession, fundamentalism... (I could be accused of it myself, some days of the week.) But I don't think it's a new stage on Andrej's list; it's stage 1, for someone going in the other direction. $\endgroup$ – Peter LeFanu Lumsdaine Jun 20 '10 at 8:40
  • 16
    $\begingroup$ Indeed, the five stages present a process of growth which end with the liberation from a difficult period in one's life, such as death, classical mathematics, drugs, or commutative groups. What Charles described goes in the opposite direction when an imprisoned soul finds its purpose in a crusade that turns out to be just as confining as the original prison. $\endgroup$ – Andrej Bauer Jun 20 '10 at 11:11
12
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ This is a pedantic point, but since we are talking about "non-standard" mathematics here, I thought the Principle of Continuity underwent a revival with the transfer principle in the context of hyperreal numbers and nonstandard analysis? Not that this says anything about whether or not we should accept or reject or make optional the law of the excluded middle, but I just wanted to point out that your claim that the Principle of Continuity "dissolved at the hands of Weierstrass" seems like an overstatement, especially considering many of the simple proofs afforded by "nonstandard" analysis. $\endgroup$ – Chill2Macht Jul 21 '16 at 22:51
10
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ In case it needs to be said for anyone: the argument underlying "Russell's paradox" is intuitionistically valid. This is fairly well-known and is of course related to Cantor's theorem, also intuitionistically valid, that a set cannot surject onto its power set. See for example page 8 of pdfs.semanticscholar.org/44d1/… $\endgroup$ – Todd Trimble May 24 '18 at 17:00

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.