# If you used intuitionistic logic in real life, would you not sound absurd?

Intuitionistic logic does not include the law of the excluded middle and double-negation elimination.

I imagine a real-life conversation with an intuitionist might go like this:

• Amy said you didn't go to school yesterday.
• She was wrong about it though!
• So you did go to school?
• What makes you say that?

Presumably, you know `(went to school)`. Since intuitionistic logic includes

``````A → ¬¬ A
``````

but not

``````¬¬ A → A
``````

this allows you to conclude and state `¬¬ (went to school)` ("she was wrong"), however the implication by your interlocutor `¬¬ (went to school) → (went to school)` may be a surprise.

If intuitionistic logic is a valid way to mechanise reasoning, why does it seem so absurd in a real-life situation?

In the above scenario, what additional knowledge would allow you to not be surprised by `¬¬ (went to school) → (went to school)`?

• Comments are not for extended discussion; this conversation has been moved to chat. Sep 20, 2020 at 6:54
• Lying about something only means that you are intentionally telling falsehood. However, that does not mean that your statement is actually false. If you base your lie on a false belief, you may very well speak the truth when lying about it. Sep 21, 2020 at 7:25
• @cmaster-reinstatemonica Good point. I'll update the dialog.
– MWB
Sep 21, 2020 at 15:55

As Conifold comments, a real-life intuitionist would not shy away from assuming LEM ... when appropriate. Intuitionism merely permits the failure of LEM, it doesn't assert that it always occurs. For example, consider equality: in intuitionistic mathematics, equality is decidable (= subject to LEM) in the context of the natural numbers but usually not in the context of the real numbers. So things are "noticeably less LEMy" when we move from a concrete setting like N to a more mysterious one like R.

This is all to say that silly conversations like the one you outline are silly precisely because our intuitionist is shying away from LEM in a context where they have no reason to do so. To see the various species of logic in action, we need to search for assertions or arguments which are genuinely messy, for example:

• They involve reference to things which are unknowable, or very difficult to know: e.g. how meaningful is the question of how many angels can dance on the head of a pin?

• They involve vague predicates, or vagueness in some other way, in such a way that both the assertion and its negation seem too strong in some sense: e.g. is "I am short" true or false?

• They refer to entities which do not exist: e.g. in what sense is "Sherlock Holmes lived in France" a false sentence?

• They are somehow intrinsically paradoxical: "This statement is false," of course, is the standard example, but there are others.

• They rest on assumptions which are individually "highly justified" but which cannot simultaneously be true: my personal favorite example of this is the question of the extent to which we can meaningfully comfortably use physical theories which are known to play poorly with each other.

There are ideas in logic addressing each such phenomenon, and many others besides, both from the point of view of trying to accommodate the weirdness in a particular logic (e.g. classcal logic) and from the point of view of searching for a more natural logic for that context. Intuitionism crops up here, but so do many-valued and fuzzy logics, relevance and paraconsistent logics, and so on. Logical pluralism emerges in this context as at least a decent candidate: that there is no single logical system appropriate to all situations (and conversely that we can learn a lot about a situation by figuring out what sort(s) of logic make sense in it).

(For what it's worth, my own stance is definitely pluralistic; in fact, I would argue that "logic" is one of a handful of ideas which are both mathematically fruitful and fundamentally un-formalizable, other big ones including "number," "space," and "set/property/collection/..." - and one surprising-to-me non-example being "effective calculability." But that's just, like, my opinion, man.)

• `... when appropriate` A concrete example would help (Please see the edit)
– MWB
Sep 19, 2020 at 0:17
• @MaxB I'm not sure I understand the edit. The intuitionist wouldn't respond as you indicate since a lifetime of experience would indicate to them that "went to school" behaves in a pretty Boolean fashion. They don't exist in a vacuum, they're allowed to use knowledge about the world to avoid pointless skepticism. (Or are you asking for an example of a situation where an intuitionist would reject an LEM claim?) Sep 19, 2020 at 20:29
• The intuitionist wouldn't respond as you indicate since a lifetime of experience would indicate to them that "went to school" behaves in a pretty Boolean fashion -- But doesn't this seem ineffective? What if there is a new concept (e.g. "bought milk"). Would you be unable to assert LEM until you acquired enough experience with that concept?
– MWB
Sep 19, 2020 at 21:28
• @MaxB If a genuinely, completely new concept were to arise, and not something easily connected with existing experience, yes, a person might be hesitant to commit to its being totally black-or-white without some more information. There's also the option of starting with LEM and later discarding it. You seem to be looking at a maximally dogmatic intuitionist - maybe that's a bit of a strawman? Sep 19, 2020 at 21:49
• A good note: \$\neg \neg (P \vee \neg P)\$ is tautological in intuitionistic logic. Meaning the LEM may not always be verified, but it is never, falsified. This is because IL is a strict weakening of classical logic, and there is obviously no counterexample to LEM in CL. Sep 20, 2020 at 3:55

Propositions in intuitionistic logic are probably best understood as statements about provability. P ʌ Q means that you can prove P and prove Q, ¬P means that from P you can derive a contradiction, ∃x.P(x) means that you can exhibit a particular x and a proof of P(x) for that x, and so on.

There is a law of noncontradiction because there can't be a proof of P and also a proof of ¬P, but there is no law of excluded middle because you may be unable to prove either one. There is a law of double negation introduction because if you can prove P then you can prove that there's no proof of ¬P, but there is no law of double negation elimination because if you can prove that there's no proof of ¬P, you may still be unable to prove P.

Your conversation would be truer to the spirit of intuitionistic logic if you replaced "lied about" with "couldn't prove". With that change, it doesn't seem absurd, just a bit Bart-Simpson-ish.

• Suppose you already said "lied about". What prevents you from saying the absurd last thing? (See the edit)
– MWB
Sep 18, 2020 at 21:09
• @MaxB I think it depends on how the conversation is encoded in the logic, and what axioms you have about attendance, etc. You can't prove P ∨ ¬P for arbitrary P but you can prove it of some specific assertions. I'm not sure I believe that "I went to school" has an unambiguous truth value in real life (especially in the current pandemic), but you can prove ∀a,b,c∊N. (a+b=c ∨ ¬(a+b=c)) from Peano-like axioms, for example. Sep 18, 2020 at 22:02
• Your second paragraph is false. It is entirely possible for a consistent formal system to prove itself inconsistent, namely to prove that there is a proof of "0=1" and a proof of "0≠1". Sep 19, 2020 at 3:24
• @benrg See if this link strengthens your answer, my friend: < core.ac.uk/display/24943925 >. :) ^^ :D 👍🏻👍🏻👍🏻👍🏻👍🏻 Sep 19, 2020 at 13:00
• @usuário21820 If it's consistent, then no. If you believe that it's consistent, then that's another five hundred. Mathematicians cannot prove that ZFC is consistent using ZFC, for example. So they can relatively assume ZFC consistency, but not prove it is using ZFC. For a theory to be consistent is literally not to be inconsistent. Aug 1, 2021 at 2:20

You give the example:

``````    Amy said you didn't go to school yesterday.
So you did go to school?
What makes you say that?
``````

The issue here is that typically you would not say that Amy lied unless you knew that what she said was false, and the implicature would be that you know what she said was false because you know you went to school.

To address the question more generally, the intuitionist is happy to accept that there are plenty of cases where A or ¬A is true. They object to this being called a law, i.e. to the claim that it is always and everywhere true, no matter whether we can tell if A is true or not. The intuitionist is committed to accepting A or B only when there is a proof or warrant for accepting A or a proof or warrant for accepting B. However, it is implausible to apply this to real-life situations because in general there are several ways in which you can know the disjunction A or B without knowing which.

• Somebody you consider to be a reliable source of information might simply tell you that A or B is true.

• It might arise from observation. You glimpse a small furry animal running across a field and remark, "that is either a rabbit or a hare". You don't know which, because you lack the expertise to distinguish, or because you didn't get a good enough look, but you know it is one or the other.

• Another case arises because of considerations of vocabulary. Suppose somebody speaks a language that has a word for 'sibling', but no word for 'brother' or 'sister'. Instead they will say 'male sibling' or 'female sibling'. Now suppose in your language there are words for 'brother' and 'sister', but no word for 'sibling', so you are forced to translate 'sibling' as 'brother or sister'. If a speaker of this language tells you they have a sibling, you know they have a brother or sister but not which. More importantly, it is not even clear what counts as a disjunction. 'Brother or sister' is disjunctive in your language but not theirs.

The upshot is that intuitionistic logic is weird when applied outside its usual boundaries of constructive mathematics and computation. In particular, there are common and unobjectionable forms of reasoning that are classically valid but not intuitionistically valid. For example,

if A then B; if not A then B; therefore, B.

And,

Not everything is F; thefore, something is not F.

• Suppose you already said "lied about". What internal axioms would prevent you from saying the absurd last thing? (See the edit)
– MWB
Sep 18, 2020 at 21:12
• An intuitionistic version might go something like: Amy said you didn't go to school yesterday. Amy is a compulsive liar and you can never know whether what she says is true or not. So you did go to school? You have no proof of that. Sep 19, 2020 at 1:22
• Humans say 'yes'/'no'. They don't restrict themselves to 'have proof' / 'don't have proof'. If you did go to school `A`, you should have no trouble using IL to assert `¬¬A`, but `¬¬A → A` by your interlocutor will seem strange to you (unless you have some extra axioms)
– MWB
Sep 19, 2020 at 1:38
• The natural way to understand intuitionistic logic (called the BHK interpretation) is that it is concerned with provability or warranted assertability, rather than with truth and falsehood. So an intuitionistic P means I can prove P, and ¬P means I can prove that there is no proof of P. Then, ¬¬P means I can prove that there is no proof that there is no proof of P, which of course is weaker than proving P. Sep 19, 2020 at 12:36

There are ways we could apply normal propositional logic that might seem insane. We might utter a contradiction (any contradiction), look our interlocutor squarely in the eye, and then confidently state, "Therefore, a cedar tree draped with polkadot cloth strips ought to be the first democratically elected leader of [insert country name]," or any other unrelated conclusion.

Granted, one doesn't normally use logical explosions as actual streams of argument, but...

Or we might think "if" and "not" and "and" and "or" are all separate, but then we speak with someone who has come up with a natural-language syntax based on the Sheffer stroke. Idk how that would sound spoken aloud but it could seem "insane," perhaps.

In principle, our sense of logic affects our standards of insanity so any substantive deviation from our sense of logic can seem insane.

• One could argue that "therefore" in natural language does not correspond to →in FOL (It might be related to causality instead, but don't quote me)
– MWB
Sep 18, 2020 at 21:19

Here's a discussion that might help:

Boss: EMPLOYEE! Did you complete that very important assignment I told you to do yesterday?

Employee: What? You didn't give me a new assignment yesterday! In fact, you weren't even in town.. you were still on vacation, right?

Boss: Look, either you completed the assigned task or you failed to complete the assigned task. Did you complete it?

Employee: No, there wasn't an.. [interrupted]

Boss: ..[interrupting] NO EXCUSES! If you didn't complete it the assigned task, then you failed to complete the assigned task. We're docking your pay!

Employee: Again, Mx. Boss, there wasn't an assignment! You were on the beach without any mobile communication! Look, here's a memo you sent out a week ago informing us you wouldn't be reachable until today!

Boss: Look, employee.. there's this little thing called the Law of Excluded Middle: something's either true or it's not; there's no alterative. So if you didn't complete the assigned task, then you must've failed to complete the assigned task. There's no possible alternative.

Employee: But that's the point of incomplete logic!: we sometimes have things that aren't true or false. For example, I neither succeeded nor failed to complete the assigned task, because, again – THERE WAS NO ASSIGNED TASK IN THE FIRST PLACE!

Boss: You silly employees and your silly nonsensical excuses! You're lucky you have me. Anyway, I know that I've been hard on you, so I'm giving you a real treasure: the world's only 50-tonne golden statue of the taste of a fresh summer ballad, made entirely of platinum and weighing only 10 pounds!

Employee: ....what....

Employee: It can't be unreceived.. there's no such thing.. that doesn't even begin to make sense..

Boss: You didn't not receive it? Awesome, then you must've received it! The Law of Excluded Middle wins again! But, yeah, you're going to need to pay gift taxes on it, just so ya know.

Later that day:

Boss: Everyone, big news! I proved that 1 is bigger than 2!

Employee: Are you sure that you're okay?

Boss: Yes, yes, I'm great! Better than ever! See, we merely define X, which is a number that's greater than itself plus 2, and.. [interrupted]

Employee: [interrupting] Yeah, I think I see where you're going with this. And that'd be great and everything, except there's no number that's greater than itself plus 2, so that doesn't work.

Boss: So you're saying that X + 1 isn't greater than X + 2?

Employee: No, it's not not greater. But that's moot as there's no such X in the first place.

Boss: If you agree that X + 1 isn't not greater than X + 2, then you agree that X + 1 is greater than X + 2. Then we subtract X from both sides, proving that 1 is greater than 2! Yay for the Law of Excluded Middle!

• Nice examples, though, FTR: properly applied classical logic does not allow you to prove 1>2. Sep 20, 2020 at 0:07

As pointed out by Noah Schweber, since LEM holds for decidable statements, we need something suitably complex to get a good example. A good starting point are existentially quantified statements. Asserting that ∃x P(x) in intuitionistic logic means being able to actually provide a witness. On the other hand, ¬∃x P(x) means being able to derive a contradiction from the putative existence of a witness. As such (∃x P(x)) ∨ ¬(∃x P(x)) will usually not be accepted.

So, in a slight modification of the example from the question, let us consider the statement "Pete went to the pub or Pete didn't." - which indeed seems absurd. Lets unravel it a bit: "Pete went to the pub" will often mean "There is a pub that Pete went to.", so we have found our existentially quantified statement.

The statement the intuitionist does not subscribe to regarding Pete's pub crawling is actually "Either Pete went to a pub (and I could tell you which one), or I can derive a contradiction from the idea that Pete did go to a pub." This statement indeed isn't one that would appear necessarily true. Note that the intuitionist can also express that Pete definitely went to a pub, but that they don't know which one. This is just ¬¬∃x P(x).

• `we need something suitably complex to get a good example... "There is a pub that Pete went to.", so we have found our existentially quantified statement. ` -- This sounds like a straw man fallacy. Why not use an existing, known pub? Or the example in the Q for that matter?
– MWB
Sep 22, 2020 at 14:23
• @MaxB Because, to me at least, "Pete went to the Winchester yesterday" feels like decidable statement, and LEM works for decidable statements.
– Arno
Sep 22, 2020 at 14:31
• @MaxB Actually, this is the opposite of a straw man argument.
– Arno
Sep 22, 2020 at 14:33

In the interpretation of Brouwer-Heyting-Kolmogorov, we are concerned about whether a sentence has proof or not. Not whether a sentence is true or not. Focus is proof, robust evidence that something counts.

Much more sensible, in my view

Simple answer, although it's for you to decide whether this sidesteps the question you actually wanted to ask: Amy could be lying but also have incorrectly modelled the world.

She may have lied that you didn't go to school, but maybe she only thought you went to school when in fact you didn't. Then she is still lying (that is, she said something she believed to be false, with the intention to mislead), but you still didn't go to school.

• IL includes A → ¬¬A as @Conifold pointed out, and you know A (went to school), as part of the question, so you know she's lying ¬¬A
– MWB
Sep 19, 2020 at 19:52
• Oh, sorry, I missed the "you actually did go to school". Sep 19, 2020 at 22:18