Exercise requires em

Stream: general

[Bjørn Kjos-Hanssen]

The last exercise at https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html#exercises seems to require Excluded Middle. After all, if we imagine truth values 0, 0.5, and 1, and

$$\neg (0.5)=0.5$$

then

$$\neg (A\leftrightarrow \neg A)$$

is not a theorem. So the problem should be moved to the next chapter (Classical Reasoning)?

[Reid Barton]

This definitely doesn't require any classical axioms. A lot of people get tripped up by this (it's a tricky argument), but most of them don't give countermodels! So I'm not sure what is happening here.

[Mario Carneiro]

three valued logic is not a model of intuitionistic logic

[Bjørn Kjos-Hanssen]

OK thanks... I'll reconsider it then

[Yury G. Kudryashov]

Hint:

example {A : Prop} (h : A → ¬ A) : ¬ A := sorry

[Bjørn Kjos-Hanssen]

oh right... you get A and not A, which is absurd

[Mario Carneiro]

for example 0.5 -> 0 is false (value 0) but is the same as not 0.5 (value 0.5)

[Mario Carneiro]

if you try to interpret 0.5 -> 0 as 0.5 then 0.5 -> 0.5 -> 0 comes out true, which is bad

[Bjørn Kjos-Hanssen]

nice...