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

[Vaughan Pratt]

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.

See http://en.wikipedia.org/wiki/Descriptive_complexity

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.

Vaughan Pratt