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

[Daniel Leivant]

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