[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: TCC's

Let me clarify my examples and arguments related to the unprovable TCC of
Joe Hurd. I interpreted this question to mean "can you have valid results
in PVS if you ignore unprovable TCC's?"  As you have pointed out in your note
on this matter, sometimes it may be the case that a theorem is valid even
though the TCC's are unprovable (particularly in the case when the information
is really available, but perhaps a formula needs to be reordered so that
dependent information appears beforehand in the context of the generated TCC,
and thus the TCC becomes provable). Much more common, as your experience shows
(and I heartily agree), the theory with unprovable TCC's is just plain wrong.
The point of my examples was simply to show that ignoring unprovable TCC's can
lead to unsoundness, even when you do not directly reference the unproven TCC's.