# FOM: a question re. completeness

wtait@ix.netcom.com wtait at ix.netcom.com
Wed Feb 4 09:43:05 EST 1998

Kanovei 2/3/98 write in response to Detlefsen's query
>I would suggest
>
>--------------
>T is consistency-complete iff for every sentence s of the
>language of T that is not provable in T, the following is
>a theorem of T:
>if Prov_T(s) then \neg Consis s
>--------------
I assume that he means \neg Consis_T and this seems to be what Mic
intended. Then PA is not consistency-complete. Here is a witness, though
probably not the simplest. Choose S so that S \coimplies [Prov(S)
\implies Prov(negS)] is a theorem of PA. S is not a theorem, since
otherwise Prov(S) would be; hence so would Prov(\negS) and PA would prove
its own inconsistency. So on the assumption of consistency-completeness,
Prov(S) \implies Prov(0=1) is a theorem. But so is Prov(0=1) \implies
Prove(negS). Hence, Prov(S) \implies Prov(\negS) is a theorem. But S is
the fixed point for this; so S is a theorem.

Bill Tait