[FOM] Proof Assistants and Conjectures (reply to Chow)
leivant at cs.indiana.edu
Sat Jan 17 12:07:20 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. All mathematicians working in this area have a very robust
>sense of what P != NP means and no confusion about the equivalence of k
>any formalizations; but can anyone suggest some statement which is
>significantly easier to formalize which is equivalent to P != NP ?
>(The proof of equivalence can be as complicated as you like.)
NP = existential second order
[Immerman, Information and control 1986, 68-86]
P = universal second order with "bounded" matrix
[Leivant, Descriptive characterizations of computational complexity.
Second Annual Conference on Structure in Complexity Theory.
IEEE Computer Society, Washington, 1987, 203--217.
[Leivant, Journal of Computer and System Sciences 39 (1989) 51--83]
The conference version gives a slightly broader condition on the matrix,
that includes duals of Horn formulas.
Closure under complementation yields
P = existential second order with Horn matrix
This was proved independently also in [Graedel, STACS 1991, Springer
LNCS 480, 466-477]
best - Daniel
More information about the FOM