Zulip Chat Archive

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

¬(0.5)=0.5 \neg (0.5)=0.5

then

¬(A¬A)\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: Dec 20 2023 at 11:08 UTC