FOM: request for info

[Sam Buss]

   Steve Cook is of course correct that his proof of the formalization of
Godel incompleteness in PV is probably the best known, in the
sense of being carried out the weakest system.  His arguments
also apply to any "reasonable" system which contains PV.  It 
predates the two examples I mentioned, and I was remiss in not
recalling this before sending my last message.

   In addition, his PV result had implications for propositional proof
systems.  In particular, one therefore *conjectures* that there are no
polynomial size extended Frege proofs of the partial consistency
statements for PV.   To explain what this means: a "extended Frege
proof" system is a textbook-style proof system for propositional logic,
based w.l.o.g. on modus ponens, with the size of an extended Frege
proof defined to equal the number of lines in the proof.    And the
partial consistency statements for PV are tautologies C_n expressing
the non-existence of n-symbol PV proofs of a contradiction.
   The hope was that from this kind of argument, Godel's incompleteness
theorems could have provided a proof that P is not equal to NP (a still
un-realized hope of course).  I think this is still the main motivation
for studying Godel incompleteness in weak systems.

 --- Sam