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
```

Thoughts please? Thank you!

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

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 *)
```

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.

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