## Stream: general

### Topic: Exercise requires em

#### Bjørn Kjos-Hanssen (Oct 02 2020 at 19:47):

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 (Oct 02 2020 at 19:55):

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 (Oct 02 2020 at 19:57):

three valued logic is not a model of intuitionistic logic

#### Bjørn Kjos-Hanssen (Oct 02 2020 at 19:59):

OK thanks... I'll reconsider it then

#### Yury G. Kudryashov (Oct 02 2020 at 19:59):

Hint:

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


#### Bjørn Kjos-Hanssen (Oct 02 2020 at 20:00):

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

#### Mario Carneiro (Oct 02 2020 at 20:02):

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

#### Mario Carneiro (Oct 02 2020 at 20:02):

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 (Oct 02 2020 at 20:03):

nice...

Last updated: May 16 2021 at 05:21 UTC