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 lists.cam.ac.uk
[mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of John
Munroe
Sent: Wednesday, March 23, 2011 8:32 AM
To: isabelle-users at cl.cam.ac.uk
Subject: [isabelle] A general TP/logic question

Hi,

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
John






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