Email Gateway (Aug 18 2022 at 19:41): Email Gateway (Aug 18 2022 at 19:41):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
I have the following lemma:
lemma "(¬ (∀ x . P x)) ⟹ (∃ x . ¬ P x)"
apply (rule exI)
apply (rule notI)
apply (erule notE)
apply (rule allI)
apply assumption
After the the rule "apply (rule allI)" the goal becomes:
⋀x. P ?x ⟹ P x
I do not understand why "apply assumption" fail at this point.
I would expect that ?x is unified with x and the proof succeed.
Best regards,
Viorel Preoteasa
Email Gateway (Aug 18 2022 at 19:41):From: Lawrence Paulson <lp15@cam.ac.uk>
Such a step would not be sound. You can only unify ?x with terms containing no bound variables. Variable capture is never allowed.
Your example is quite tricky to prove in a natural deduction calculus. Of course, it's trivial if you use automation.
Larry Paulson
Email Gateway (Aug 18 2022 at 19:42):From: Alfio Martini <alfio.martini@acm.org>
Dear Viorel,
If I am not wrong, this is a classical conjecture. Here goes a
possible proof:
lemma "(¬ (∀ x . P x)) ⟹ (∃ x . ¬ P x)"
apply (rule ccontr)
apply (erule notE)
apply (rule allI)
apply (rule ccontr)
apply (erule notE)
apply (rule exI)
apply (assumption)
done
Best!
Email Gateway (Aug 18 2022 at 19:43):From: Makarius <makarius@sketis.net>
We've been an the same point just yesterday in our Isabelle tutorial at
Paris Sud point, but nobody could give me the proof on the spot. See
http://www.lri.fr/~wenzel/Isabelle_Orsay_2012/Calculation.thy Exercise (2)
about the Drinker's principle.
The idea was to play with proof structure and automated tools to bridge
the gaps, and show the possibilities and limitations of this approach.
The question of the assignment "Do you believe the proof?" (a skeleton
involving 3 "blast" steps) was answered negatively by everybody.
Afterwards I've made a fully explicit Isar proof, and managed to convince
at least half of the audience that this is correct classical nonsense.
To complete my own exercise from yesterday, here is now de_Morgan as above
(using the more generic rule classical instead of ccontr) together with
the explicit version of the Drinker's principle:
lemma de_Morgan:
assumes "¬ (∀x. P x)"
shows "∃x. ¬ P x"
proof (rule classical)
assume "¬ (∃x. ¬ P x)"
have "∀x. P x"
proof
fix x show "P x"
proof (rule classical)
assume "¬ P x"
then have "∃x. ¬ P x" ..
with ¬ (∃x. ¬ P x) show ?thesis ..
qed
qed
with ¬ (∀x. P x) show ?thesis ..
qed
theorem "∃a. drunk a ⟶ (∀x. drunk x)"
proof cases
assume "∀x. drunk x"
fix a
have "drunk a ⟶ (∀x. drunk x)"
using ∀x. drunk x ..
then show ?thesis ..
next
assume "¬ (∀x. drunk x)"
then have "∃a. ¬ drunk a" by (rule de_Morgan)
then obtain a where "¬ drunk a" ..
have "drunk a ⟶ (∀x. drunk x)"
proof
assume "drunk a"
with ¬ drunk a show "∀x. drunk x" by contradiction
qed
then show ?thesis ..
qed
For demonstration purposes in such Pure examples, I usually refer to
previous facts literally with prop, to avoid the Spaghetti tendency of
named references like , , or 1, 2, 3 etc.
Makarius
Email Gateway (Aug 18 2022 at 19:43):From: Alfio Martini <alfio.martini@acm.org>
Dear Makarius,
The corresponding Isar proof I had done, which follows the procedural one
below was this one:
lemma
assumes p: "(¬ (∀ x . P x))"
shows "(∃ x . ¬ P x)"
proof (rule ccontr)
assume h1: "¬ (∃x. ¬ P x)"
have "∀x. P x"
proof (rule allI)
fix x0
show "P x0"
proof (rule ccontr)
assume "¬ P x0"
from this have "∃ x. ¬P x" by (rule exI)
with h1 show False by (rule notE)
qed
qed
with p show False by (rule notE)
qed
But since I am still learning Isar, it does not look as elegant as yours!
best!
Last updated: Nov 21 2024 at 12:39 UTC