[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.