[FOM] Proof Assistants and Conjectures (reply to Chow)
joeshipman at aol.com
Sat Jan 17 16:46:54 EST 2009
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).
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.
More information about the FOM