[FOM] Proof Assistants and Conjectures (reply to Chow)
pratt at cs.stanford.edu
Sat Jan 17 12:54:55 EST 2009
Joe Shipman wrote:
> P != NP is not so easy to formalize because of the background
> necessary to define a model of computation and the complexity classes
> P and NP.
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