On Formally Undecidable Propositions of Nondeterministic Complexity and Related Classes
Martin Kolář
cs.CC
Apr 8, 2026 · v1
TL;DR
Formalizes in Lean 4 an impossibility result about a sound, complete, decidable arithmetic proof system tied to the NP definition; repository provided.
Abstract
The definition of \NP\ requires, for each member language $L$, a polynomial-time checking relation $R$ and a constant $k$ such that $w \in L \iff \exists y\,(|y| \leq |w|^k \wedge R(w,y))$. We show that this biconditional instantiates, for each member language, Hilbert's triple: a sound, complete, decidable proof system in which truth-in-$L$ and bounded provability coincide by fiat. We show further that the polynomial-time restriction on $R$ does not exclude Gödel's proof-checking relation, which is itself polynomial-time and fits the definition as a literal instance. Hence \NP, taken as a totality over all polynomial-time $R$, contains languages for which the biconditional asserts a property that Gödel's First Incompleteness Theorem prohibits. The semantic definition of \NP\ is unsatisfiable, for the same reason that Hilbert's Program is.
Problem
The paper argues that the semantic definition of NP is unsatisfiable. Its claim is that the NP biconditional, instantiated with Gödel's polynomial-time proof-checking relation, reproduces Hilbert's sound-complete-decidable triple, which Gödel's First Incompleteness Theorem forbids.
Approach
Gödel's ProofOf relation is shown to be polynomial-time under a string encoding, which makes it a valid NP checking relation. Bounded-provability languages L_k are then defined for consistent theories interpreting Robinson arithmetic. A diagonal argument is used to derive the contradiction. The core impossibility result (no_arithmetic_completeness_triple) is formalized in Lean 4.
Results
Three results are machine-checked in Lean 4, relying only on the standard axioms propext, Classical.choice and Quot.sound. The polynomial-time property of ProofOf and the interpretive identification with the NP biconditional are not formalized.
