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.

翻译：若要将一个算法视为决策问题的实际有效解，则该算法必须在某种构造性且“可信”的理论（如PA或ZF）中可验证。本文通过一类与形式理论不一致性证明相关的决策问题证明：在此构造性限制下，存在合理的论证表明，存在可形式化证明属于NP类的决策问题，且存在显式构造的多项式时间算法可识别正确解，但不存在显式构造且可验证的求解算法。虽然这些论证并未在“可信”形式理论中提供传统意义上的P对NP问题证明，但可认为其解决了该问题的构造性版本。