Stream: Beginner Questions

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

Jiahong 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.

Jiahong 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.

Jiahong Lee (Aug 12 2021 at 15:48):

Hi @Wenda Li,

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

Jiahong Lee (Aug 13 2021 at 07:50):

Hi all,

I found a solution to lemma (A ∨ ¬A) in the Isabelle/Isar Reference Manual by Wenzel (2021), Section 2.3.4 "Classical logic". Very similar to my original question, so I adapted it to solve my problem:

lemma "¬¬ (A ∨ ¬A)"
proof (rule notI)
  assume n1: "¬ (A ∨ ¬A)"
  have "¬ A"
  proof (rule notI)
    assume A
    then have "A ∨ ¬A" by (rule disjI1)
    with n1 show False by (rule notE)
  qed
  then have "A ∨ ¬A" by (rule disjI2)
  with n1 show False by (rule notE)
qed

On hindsight, my problem is not knowing that I can prove an intermediate result, i.e. having a proof block following a have statement. It's eye-opening and I find it quite elegant to be able to do so. (Thank you to Isabelle/Isar designer!)

Hope that you find this useful! :wink:

Notification Bot (Aug 13 2021 at 07:51):

Jia Hong Lee has marked this topic as resolved.

Last updated: Apr 19 2024 at 04:17 UTC