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, an unformalizable yet arguably convincing argument can be given for the existence of decision problems for which there exists an explicitly constructible algorithm recognizing correct solutions in polynomial time, but for which there exists no explicitly constructible solution algorithm. While these results 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 the natural constructive version of the problem.

翻译：若要将一个算法视为决策问题的实际可行解，则该算法必须在某个构造性且"可信"的理论（如PA或ZF）中可验证。本文通过一类与形式理论不一致性证明相关的决策问题证明：在此构造性限制下，可以给出一种虽不可形式化但具有说服力的论证，表明存在这样的决策问题——存在显式可构造的多项式时间算法能识别正确解，却不存在显式可构造的求解算法。尽管这些结果并未在经典意义上通过"可信"形式理论提供确定性的证明来解决P对NP问题，但可以认为它们解决了该问题的自然构造性版本。