Re: [isabelle] A general TP/logic question

You could try to exhibit a model of T in which 'f = g' holds and then
exhibit another model of T in which 'f = g' does not hold.  That's how
the 'parallel postulate' of Euclidian geometry was shown to be
unprovable from the other axioms.

-----Original Message-----
From: cl-isabelle-users-bounces at
[mailto:cl-isabelle-users-bounces at] On Behalf Of John
Sent: Wednesday, March 23, 2011 8:32 AM
To: isabelle-users at
Subject: [isabelle] A general TP/logic question


I have a general theorem proving/logic question: does it make sense to
have a proof obligation that checks for unprovability? For example,
the proof obligation may require that a particular sentence, like "f =
g" to be unprovable from a theory T, i.e. "T |+ f = g". Checking for
unprovability is undecidable, right? If such a constraint is
impractical, then is there a more practical formulation for checking
the same/similar property?

Thanks a lot

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.