Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] strange isabelle behaviour

Email Gateway (Aug 18 2022 at 10:55):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
I experienced some strange behaviour when using Isabelle
to check natural deduction proofs for first-order logic.

The following lemma is easily proved:

lemma "EX y. P(x_0, y) ==> EX x. EX y. P(x, y)" by auto

Hence I thought that every formula that unifies with
the above, would also be provable.
As soon as negations come into play however, I get problems.

lemma "EX y. ~ x_0 = y ==> EX x. EX y. ~ x = y" by auto

is not accepted. Why is this the case? As far as I'm concerned

?P = %(x, y). ~ x = y

unifies the two premises (and conclusions) of the two lemmas.
Thus they should both be provable.

cheers

christian

Email Gateway (Aug 18 2022 at 10:56):

From: Tobias Nipkow <nipkow@in.tum.de>
Your second lemma is unprovable because the premise and the conclusion
are not "linked" and thus talk about independent types. (Comand `refute'
would actually have spotted this.)

More to the point: you cannot expect that if some proposition is proved
automatically by method m, m will also prove any instance automaticallly

• most theorem proving methods are only complete on paper and many
  implementations explicitly give up on completeness.

Tobias

Christian Sternagel schrieb:

Last updated: May 03 2024 at 04:19 UTC