What one has to know when attacking P vs. NP

摘要

We call any consistent and sufficiently powerful formal theory that enables to algorithmically verify whether some text is a proof algorithmically verifiable mathematics (AV-mathematics). We say a decision problem L⊆Σ⁎ is almost everywhere solvable if for all but finitely many inputs x∈Σ⁎, one can prove “x∈L” or “x∉L” in AV-mathematics. We study what kind of problems related to algorithms and computational complexity are not almost everywhere solvable in AV-mathematics. We observe that this is true for all semantically nontrivial problems about programs and show several results of the kind “There exist programs that are provably algorithms for which it is neither provable that they do not work in polynomial time, nor that they do not solve SATISFIABILITY.” Finally, we prove that, if DLOG=NLOG, or BPP=PSPACE, then there exist constructive proofs for it and almost constructive in the case P=NP.