FOM: a question re. completeness

[wtait@ix.netcom.com]

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