# Is it possible to use intuitionistic logic in some everyday situations?

Intuitionistic logic is the same as the usual boolean one apart from excluding the excluded middle, that is not(p) or p is not neccessarily true, so that boolean logic is a specialisation of the intuitionistic one.

I take it evident that some parts of everyday reasoning uses classical boolean logic.

Are there any everyday situations (i.e. not mathematical ones) in which intuitionistic logic is used?

What does it mean to "use" logic? To reason in accordance with it? Is it evident we use classical logic? Is all our reasoning even formalisable as logical inference? Certainly not. Think about any reasoning that involves likely but uncertain events. This doesn't necessarily admit of an obvious translation into a simple logical framework. More esoterically, there are sentences which are "un-first-order-isable". That is, grammatical, meaningful English sentences that can't be formalised in a first-order logic. That is, you need to quantify over predicates to make them amenable to formalisation.

The upshot of this is that it probably isn't possible to consistently use logic in everyday situations, whatever logic you use.

So perhaps the question should really be: Can you replace classical logic in everyday reasoning with intuitionistic reasoning? Rephrasing: can every everyday use of classical logic be replaced with intuitionistic logic?

And the answer there is: "of course not!". Think about all the times you do reason by using excluded middle. None of these inferences will work in intuitionistic logic.

• Excellent answer. The point about the (not uncommon) inapplicability of formal logic to everyday events is an important one. Commented May 9, 2012 at 11:23
• Good critique, I should have made it clearer that I don't suppose all human reasoning is formalisable, but that some of it is evidently, and its that fragment I'm concerned with. I wasn't expecting a straight replacement of the logic, just a situation where intuitionistic logic is more reasonable. Commented May 9, 2012 at 12:43
• @Seamus "That is, grammatical, meaningful English sentences that can't be formalised in a first-order logic." Can you suggest examples? Commented May 31, 2012 at 5:37
• @GustavoBandeira For example the Geach-Kaplan sentence: Some critics admire only on another. See: en.wikipedia.org/wiki/Nonfirstorderizability Commented May 31, 2012 at 19:10
• Mm. Not convinced. For the most commonly encountered sentences, intuitionistic and classical logic coincide. (To put some formal flesh on this, in languages where recursive sentences are decidable, \$Pi^0_2\$ sentences are classical provable iff they are intuitionistically provable). It's only with formulae with a quite tricky meaning that the two logics disagree. Commented Jun 5, 2012 at 21:35

I would argue it can be used effectively as the "logic" of scientific field. Or in fact any field where we want to separate the notions of direct and indirect evidence. I would argue that that some fact p has been established is distinct from saying the (weaker) statement that it has not been established that p has not been established. The first is the assertion that p holds, while the second is something like saying that p has not been ruled out and is still possible. In a formal logic, we can represent a direct assertion as "p", while for the second indirect kind, "not not p". Classical logic collapses these two notions since it proves p if and only if not not p. On the other hand, intuitionistic logic keeps these two apart.

One small thing to note: intuitionistic logic is properly contained in classical logic. So intuitionistic logic is in fact used all the time: from p and q we have p; from p implies q and p we have q, and so on. Mathematically, we can define the intuitionistic part of classical propositional logic as that obtained from all the rules of classical logic expect for (one of the many rules equivalent to) double negation elimination. I'll rephrase your intended question then not as when intuitionistic logic is used in everyday reasonings (which is all the time!) but when it is inappropriate to use the extra power of classical logic.

• Isn't it the other way around? Classical logic is contained in intuitionistic logic, after ll we assert the Excluded Middle rather than deny it? Commented May 30, 2012 at 15:06
• Intuitionistic logic (IL) is contained in classical logic (CL) in the following sense: any p provable in IL is provable in CL, while there are q provable in CL but not provable in IL, for instance "p or not p". Commented May 31, 2012 at 1:20

Seamus answer highlights a typical misconception concerning intuitinistic logic:

So perhaps the question should really be: Can you replace classical logic in everyday reasoning with intuitionistic reasoning? Rephrasing: can every everyday use of classical logic be replaced with intuitionistic logic?

And the answer there is: "of course not!". Think about all the times you do reason by using excluded middle. None of these inferences will work in intuitionistic logic.

Because the Gödel–Gentzen translation gives a perfectly reasonable embedding of classical logic into intuitionistic logic, the answer "of course not!" seems questionable. (Note that this translation even uses the intuitionistic consequence relation, which was Gerhard Gentzen's contribution.) I used a similar translation to make sense of non-constructive results using the axiom of choice even before I knew that this translation always works. (I thought of proofs using the axiom of choice as showing that trying to disprove (of falsify) the given existence claim would be futile.)

The answer by "anonymous bro" also shows inawareness of the strength of intuitionistic logic:

I would argue that that some fact p has been established is distinct from saying the (weaker) statement that it has not been established that p has not been established. The first is the assertion that p holds, while the second is something like saying that p has not been ruled out and is still possible.

The correct (weaker) statement from intuitionistic logic would be that it has been established that the falsity of p cannot be established. The first is the assertion that p holds, while the second is something like saying that p can never be ruled out.