How to know when classical reasoning is needed?

Stream: new members

[Martin C. Martin]

Exercise 5.3.4 here asks to prove 𝑃 from ¬𝑃→(𝑄∨𝑅), ¬𝑄, and ¬𝑅. It's easy to prove ¬ ¬𝑃 intuitionistically, and it seems you need proof by contradiction to get to P. Is there a way to convince myself that it really can't be done through intuitionistic reasoning? Say, using a 3-valued truth table or something?

[Yaël Dillies]

One way to see it is that there is no way to introduce P. You have no arrow going to P, and you need one if you go constructively.

[David Wärn]

I think it's easier to justify the truth table approach. Whenever you have a special kind of partial order called a Heyting algebra, you can interpret intuitionistic logic in it. Exercise 5.3.4 is in fact equivalent to double negation elimination, so your question reduces to finding some element p of some Heyting algebra such that p < ¬¬p. Indeed the 3-element Heyting algebra {0, 1, maybe} does the job.

One simple way of understanding the 3-element Heyting algebra is by checking more generally that any bounded total order P is a Heyting algebra. Given p q : P, you define logical connectives as follows: p ∨ q is max(p,q), p ∧ q is min(p,q), and p → q is ⊤ if p ≤ q and q otherwise.

[Anne Baanen]

Yaël Dillies said:

One way to see it is that there is no way to introduce P. You have no arrow going to P, and you need one if you go constructively.

This line of reasoning is essentially true, but : P → ¬ P → Q is intuitionistically valid!

I think the correct way to argue this is to start out from the fact that polymorphic lambda terms are natural in their parameters. So you can't do case distinction on the types themselves, which is why truth tables don't work :)

[Kyle Miller]

@Anne Baanen If false is defined by its principle of explosion (which it is anyway in Lean with false.elim), then I guess even that dangerous bend can still be solved by Yael's criterion. It's just that we've now left propositional logic.

def false' := ∀ (r : Prop), r

example (p q : Prop) : p → (p → false') → q :=
λ h h', h' h _

[Yaël Dillies]

Yes of course. Because false is included in the original problem (because of the not), you need to account for its eliminator.

[Kyle Miller]

@Yaël Dillies But then doesn't that mean the original problem has two arrows to P from the two negations?

[Yaël Dillies]

Yes it has, I was wrong. But applying one of them leaves you with Q or R as a goal which you can only prove using false.elim (which doesn't buy you anything new because you didn't intro anything since last time) or or.elim (which doesn't buy you anything either, but that looks a bit fiddly at first)

[Mario Carneiro]

import tactic.itauto

-- one way to convince yourself that the theorem isn't intuitionistic:
example {p q r : Prop} (h₁ : ¬ p → q ∨ r) (h₂ : ¬ q) (h₃ : ¬ r) : p :=
by itauto -- failed

-- another way, which doesn't always work, is to use it to prove LEM
theorem foo {p q r : Prop} (h₁ : ¬ p → q ∨ r) (h₂ : ¬ q) (h₃ : ¬ r) : p := by itauto!

theorem em'' {p : Prop} : p ∨ ¬ p :=
have ¬¬(p ∨ ¬ p), by itauto,
foo (λ h, (this h).elim) not_false not_false

[Eric Taucher]

First off I am a programmer first and a newbie at proofs here and in general.

In reading this StackExchange Computer Science Q&A the part about intuitionistic logic made sense and I was wondering if it also made sense with regards to this topic.

Answer by Gilles 'SO- stop being evil'

in disjunction you can have both values present at the same time

In classical logic, yes. ... And in intuitionistic logic, to speak intuitively, when you know that A∨B is true, you know which one is true.

The idea of intuitionistic logic is that if you can prove a proposition P, it doesn't mean “P is true” (as it does in classical logic), but “I know how to prove P”. When the proposition is of the form A∨B, the way to prove A∨B must either involve a proof of A or a proof of B, plus the information of which side you chose to prove. This is not true in classical logic, which has A∨¬A as an axiom, which doesn't tell you which of A or ¬A is true or how you'd prove it. The absence of this axiom, the excluded middle, is the defining feature of intuitionistic logic compared to classical logic.

[Anne Baanen]

Indeed, there is a rigorous way to say the above, in there is a modal companion of intuitionistic logic. This is a translation into classical logic + the S4 modal axioms, where you put a box (standing for "I know a proof of") in front of every subexpression of a proposition. So A ∨ ¬A becomes []([]A ∨ []¬[]A). You can prove using the S4 axioms it is equivalent to put a box only in front of ¬ and →, so you get []A ∨ []¬[]A: "either I know a proof of A or I know a proof that there is no proof of A".

[Anne Baanen]

So if you know modal logic but not intuitionistic logic, this might help to give a bit of intuition :)

[Trebor Huang]

A more elementary way to do this is to consider any topology, say the usual one on the real line.

So false is interpreted as the empty set, true the whole set. Conjunction/disjunction corresponds to the usual intersection/union. And p -> q means (R \ p) ∪ q, and take the interior. Note that this ensures that every set you deal with is an open set.

[Trebor Huang]

So in this case Q, R are empty, and not P -> (Q or R) means the closure of P is the whole set, which by no means implies that P is the whole set.