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

Thoughts please? Thank you!

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