[FOM] Proof Assistants and Conjectures (reply to Chow)

[joeshipman@aol.com]

This is still unsatisfactorily complicated. At least it is true that 
the statement of P=?NP is very robust and nobody has any doubt about 
what precisely it says.

Another example of a statement which is very complicated to formalize 
but which has a simple abbreviation that everyone understands is V=L 
(those who reject ZF-style set theory on semantic grounds will of 
course disagree, but my point is that even if you accept ZF-style set 
theory V=L is very hard to fully formalize).

-- JS


-----Original Message-----
From: Vaughan Pratt <pratt at cs.stanford.edu>

P =? NP has the same answer as the question whether first-order logic
with a least fixed point operator in the presence of a linear order is
equivalent to existential second-order logic.  Polynomials, time, and
models of computation do not enter into the question when phrased that
way.  Not that this necessarily makes the definition any easier, Goedel
had quite a struggle formulating his incompleteness theorems.