Stream: Beginner Questions

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


view this post on Zulip Jia Hong 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:

view this post on Zulip Notification Bot (Aug 13 2021 at 07:51):

Jia Hong Lee has marked this topic as resolved.


Last updated: Jul 15 2022 at 23:21 UTC