Reducing P vs. NP to SAT The following question uses ideas from cryptography applied to complexity theory. That said, it is a purely complexity-theoretic question, and no crypto knowledge whatsoever is required to answer it.

I deliberately write this question very informally. Lacking details, it is possibly stated a bit incorrectly. Please feel free to point out the corrections in your answers.



In the following papaper:
Nonmalleable Cryptography, Danny Dolev, Cynthia Dwork, and Moni Naor, SIAM Rev. 45, 727 (2003), DOI:10.1137/S0036144503429856,
the authors write:


  Suppose researcher A has obtained a proof that P ≠ NP and wishes to communicate this fact to professor B. Suppose that, to protect herself, A proves her claim to B in a zero-knowledge fashion...


There are several standard NP-complete problems, like satisfiability (SAT), Graph-Hamiltonicity, and Graph-3-Colorability (G3C), for which zero-knowledge proofs exist. The standard way of proving any NP-theorem is to first reduce it to an instance of the aforementioned NP-complete problems, and then conduct the zero-knowledge proof.

This question pertains to such reduction. Assume that the P vs. NP is settled in any of the following ways:


P = NP
P ≠ NP
P vs. NP is independent of the standard axiomatic set theory.


Let σ denote the proof. Then, P vs. NP is in an NP language (since there exists a short proof for it). The reduction from the theorem (say, P ≠ NP) to the NP-complete problem (say SAT) is independent of σ. That is:

There exists a formula ϕ which is satisfiable if and only if P ≠ NP.

This is well beyond my imagination! It seems that, even if we are given the proof σ, it is unlikely that we can construct such formula ϕ.


  Could anyone shed some light on this?


In addition, let L be an NP language in which P vs. NP lies. The language is consists of infinitely many theorems like P vs. NP, of arbitrary sizes.


  What is a candidate for L? 
  Can L be NP-complete?
The way to view testing a math statement (e.g., a resolution of P vs NP) as a question of the form "is formula .. satisfiable" is the following:

Fix some axiom system.
Given a string of length n, whether the string is a proof for the math statement in the axiom system, is something one can define in a straightforward manner:
the string should consist of propositions. Each proposition should either be an axiom, or should follow from the previous propositions by one of the inference rules.

It's not a problem to define a Boolean formula that verifies all this.
All you should know is the length n of the proof!