A class of decision problems related to inconsistency proofs for formal theories is used to show that under a constructive interpretation of computational complexity classes, an assumption referred to as the MW thesis implies that one may explicitly construct decision problems in NP which are not algorithmically solvable. In particular, in this interpretation the MW thesis implies P $\neq$ NP. It is argued that MW is a naturally valid, yet also naturally unformalizable principle.

翻译：通过一类与形式理论不一致性证明相关的判定问题，本文证明在计算复杂度类的构造性解释下，一个被称为MW论题的假设意味着我们可以显式构造出NP类中无法通过算法求解的判定问题。特别地，在此解释框架下，MW论题可推出P ≠ NP。本文论证MW论题是一个自然有效却无法被形式化的原理。