Email Gateway (Aug 18 2022 at 10:32): Email Gateway (Aug 18 2022 at 10:32):From: John Ridgway <john@jacelridge.com>
How do I prove the following lemma?
lemma the_false [simp]: "\<not> (\<exists>y. ((THE x. False) = y))"
or something similar?
Peace
Email Gateway (Aug 18 2022 at 10:32):From: Peter Lammich <peter.lammich@uni-muenster.de>
John Ridgway wrote:
You cannot proof this, because the opposite is true. y="THE x. False"
witnesses that there exists such an y.
lemma "(\<exists>y. ((THE x. False) = y))"
apply (rule exI[where x="THE x. False"])
apply (rule refl)
done
Well, you cannot prove many statements about "THE x. False", but if this
lemma shall be false, you have to drop one of the rules refl or exI
(i.e. the corresponding axioms), and you usually do not want this in
your logic.
Regards
Peter
Email Gateway (Aug 18 2022 at 10:32):From: Brian Huffman <brianh@cs.pdx.edu>
If it is the case that there exists a unique x such that P x holds, then we
can prove that (THE x. P x) = x. In typical usage "THE" would only be applied
to predicates that satisfy unique existence. But it is still type correct to
write (THE x. P x) for any P, whether it has unique existence or not. Since
all functions in HOL are total, (THE x. P x) has a value of type 'a for any
P :: 'a => bool.
If P does not satisfy unique existence, then (THE x. P x) is underspecified:
Logically it could be any value of the correct type, but there is no way to
tell which one. You can only prove trivial facts about it that don't depend
on its value, for example that it is equal to itself.
Last updated: May 03 2024 at 08:18 UTC