Constructibility, computational complexity and P versus NP

If an algorithm is to be counted as a practically working solution to a decision problem, then the algorithm must must verifiable in some constructed and ``trusted'' theory such as PA or ZF. In this paper, a class of decision problems related to inconsistency proofs for a general class of formal theories is used to demonstrate that under this constructibility restriction, there are plausible arguments for the existence of decision problems which can be proved formally to be in NP, and for which there exists an explicitly constructible algorithm recognizing correct solutions in polynomial time, but for which there exists no explicitly constructible, verifiable solution algorithm. While these arguments do not solve the P versus NP problem in the classical sense of supplying a proof one way or the other in a ``trusted'' formal theory, arguably they resolve a constructive version of it.