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