## 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 that`Assume ¬ (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