## Stream: Beginner Questions

### Topic: Prove lemma "¬¬ (A ∨ ¬A)" by natural deduction

#### Jia Hong Lee (Aug 12 2021 at 12:50):

Hi, I'm a programmer by trade and just started learning Isabelle/HOL during my free time. I've been following "Isabelle for Philosophers" by Ben Blumson (2019) here since it starts with propositional logic and uses Isar-style proofs.

However, I'm stuck at Exercise 13 (page 14) proving lemma "¬¬ (A ∨ ¬A)" using natural deduction. There is a hint stating thatAssume ¬ (A ∨ ¬A) and then prove (A ∨ ¬A) by disjunction introduction from ¬A.... Ha! But I'm not even sure where the ¬A comes from :rolling_on_the_floor_laughing:

After poking around to no avail, I cheat a bit using a propositional prover, hoping to get an answer. Note: - is for negation and + is for disjunction. Typed in this --(a + -a) and got this:

assume -(a + -a).
assume a.
a + -a.
F.
therefore a ==> F.
assume -a.
a + -a.
F.
therefore -a ==> F.
F.
therefore --(a + -a).

It doesn't make sense why, after proving a ==> F and -a ==> F, it proves - (a + -a) ==> F and thus -- (a + -a). It definitely looks like it's applying disjE to a + -a when in fact it's proving - (a + -a) ==> F. That's where it loses me.

My failed attempts:

(* Exercise 13 *)
lemma "¬¬ (A ∨ ¬A)"
proof (rule notI)
assume notana: "¬ (A ∨ ¬A)"
show False
proof (rule disjE)
show "¬ (A ∨ ¬A)" using notana.
next
show ana: "A ∨ ¬A"
proof (rule disjE)
show "A ∨ ¬A" using ana .
oops

lemma "¬¬ (A ∨ ¬A)"
proof (rule notI)
assume notana: "¬ (A ∨ ¬A)"
assume A
hence "A ∨ ¬A" by (rule disjI1)
with notana have False by (rule notE)
assume "¬A"
hence "A ∨ ¬A" by (rule disjI2)
with notana have False by (rule notE)
oops

#### Mathias Fleury (Aug 12 2021 at 13:02):

Look at the State panel: the goals are not what you think there are.

#### Jia Hong Lee (Aug 12 2021 at 13:10):

Hi @Mathias Fleury ,

Tq, I'm well aware of the use of State panel. My problem is that I'm stuck after applying rule notI looking for help.

lemma "¬¬ (A ∨ ¬A)"
proof (rule notI)
assume notana: "¬ (A ∨ ¬A)"
show False
oops (* stuck here *)

#### Wenda Li (Aug 12 2021 at 13:31):

The following sketch should work:

lemma "¬¬ (A ∨ ¬A)"
proof (rule notI)
assume notana: "¬ (A ∨ ¬A)"
then show False
apply (elim notE)
apply (rule disjCI)
apply (rule notnotD)
apply assumption
done
qed

but you may need to adapt it to the Isar style.

#### Jia Hong Lee (Aug 12 2021 at 15:48):

Hi @Wenda Li,

Thank you for your pointer! I'll try it in Isar style :grinning:

Last updated: Jul 15 2022 at 23:21 UTC