pith. sign in

arxiv: 2604.07406 · v1 · submitted 2026-04-08 · 💻 cs.CC

On Formally Undecidable Propositions of Nondeterministic Complexity and Related Classes

Martin Kol\'a\v{r} This is my paper

Pith reviewed 2026-05-10 18:00 UTC · model grok-4.3

classification 💻 cs.CC
keywords NP definitionGödel incompletenessHilbert programpolynomial time verifiableundecidable propositionsproof systemsnondeterministic complexity
0
0 comments X

The pith

The semantic definition of NP is unsatisfiable because it requires each of its languages to possess a sound, complete, decidable proof system.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper demonstrates that the standard definition of the complexity class NP leads to a logical inconsistency with Gödel's first incompleteness theorem. Specifically, the requirement that membership in an NP language is equivalent to the existence of a short witness verifiable in polynomial time creates, for every such language, a formal system that is sound, complete, and decidable. This setup is exactly what Hilbert's program attempted and what Gödel proved cannot exist for sufficiently strong systems. Because Gödel's own proof-checking relation turns out to be polynomial-time and satisfies the witness bound, the definition applies to languages involving arithmetic truth, which incompleteness rules out.

Core claim

For each language L in NP the defining biconditional w ∈ L iff there exists a short y such that R(w, y) holds with R polynomial-time, forms a sound complete decidable proof system in which truth in L coincides with bounded provability. Since Gödel's proof-checking relation is itself polynomial-time and fits the bound, NP contains languages for which this biconditional asserts the existence of such a system, contradicting the first incompleteness theorem.

What carries the argument

The NP biconditional definition acting as Hilbert's triple of soundness, completeness, and decidability for truth in the language.

If this is right

  • The definition of NP cannot be satisfied for all its intended member languages without violating incompleteness.
  • NP as a class includes languages where provability in a fixed system decides truth up to polynomial bounds.
  • Similar issues apply to other classes defined via polynomial-time verifiable witnesses.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the argument holds, standard questions about whether P equals NP would need to account for this foundational inconsistency in the definition.
  • Complexity classes might require syntactic rather than semantic definitions to avoid this problem.
  • Extensions to other nondeterministic classes could reveal analogous undecidability issues.

Load-bearing premise

That Gödel's proof-checking relation is computable in polynomial time and that the length of proofs satisfies the polynomial bound |y| ≤ |w|^k for some fixed k.

What would settle it

An explicit analysis or proof that verifying the correctness of a proof in Gödel's formal system cannot be done in time polynomial in the size of the formula being proved.

read the original 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\"odel'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\"odel's First Incompleteness Theorem prohibits. The semantic definition of \NP\ is unsatisfiable, for the same reason that Hilbert's Program is.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The paper claims that the definition of NP requires for each language L a polynomial-time checking relation R and constant k such that w ∈ L iff ∃y (|y| ≤ |w|^k ∧ R(w,y)). It argues this biconditional creates a sound, complete, decidable proof system instantiating Hilbert's program. The paper further asserts that Gödel's proof-checking relation is polynomial-time and fits the NP definition as a literal instance, implying that NP contains languages for which the definition asserts a property prohibited by Gödel's First Incompleteness Theorem, rendering the semantic definition of NP unsatisfiable.

Significance. If the central claim were correct, the result would link complexity theory to incompleteness results in a way that shows the NP definition to be internally inconsistent. The manuscript attempts a direct reduction of Gödel's relation to the NP witness form, but the argument does not establish the required fixed polynomial bound on witnesses.

major comments (3)
  1. [Abstract] Abstract: the claim that 'Gödel's proof-checking relation... is itself polynomial-time and fits the definition as a literal instance' is not supported. The NP definition requires a fixed k (independent of w) such that every w ∈ L has a witness y with |y| ≤ |w|^k. For L = theorems of PA, no such fixed k exists because the shortest-proof-length function grows faster than any polynomial (via self-referential constructions or known lower bounds for combinatorial statements).
  2. [Abstract] The central derivation (that the biconditional produces a sound complete decidable system prohibited by Gödel) does not go through once the witness-length condition fails to hold for the full set of theorems. The manuscript provides no explicit construction or proof that the checking relation R for Gödel's predicate satisfies the bounded-witness form for all theorems.
  3. [Abstract] The argument invokes the semantic definition of NP without addressing that standard accounts place the set of true arithmetic sentences outside NP precisely because of the absence of a uniform polynomial witness bound.
minor comments (2)
  1. [Abstract] The abstract and title use 'Nondeterministic Complexity' without defining the term or relating it to standard nondeterministic Turing machine definitions.
  2. [Abstract] No explicit statement of the precise formal system (e.g., PA or a weaker theory) is given when invoking Gödel's theorem.

Simulated Author's Rebuttal

3 responses · 1 unresolved

We thank the referee for the detailed and insightful report. We respond point-by-point to the major comments and outline the revisions we intend to make to strengthen the manuscript.

read point-by-point responses

  1. Referee: Abstract: the claim that 'Gödel's proof-checking relation... is itself polynomial-time and fits the definition as a literal instance' is not supported. The NP definition requires a fixed k (independent of w) such that every w ∈ L has a witness y with |y| ≤ |w|^k. For L = theorems of PA, no such fixed k exists because the shortest-proof-length function grows faster than any polynomial (via self-referential constructions or known lower bounds for combinatorial statements).

    Authors: The manuscript correctly notes that the proof-checking relation for formal systems like PA is computable in polynomial time relative to the lengths of the statement and the proof. However, we accept the referee's observation that the manuscript does not supply a proof or construction establishing the existence of a fixed k that bounds the witness length for every theorem. Since no such k exists, as established by results on the growth of proof lengths, the literal application to the set of PA theorems does not hold. We will revise the abstract and relevant sections to remove the assertion of a 'literal instance' for this particular L and instead focus on the general implication of the NP definition's biconditional form for any language that does satisfy the bounded-witness condition. revision: yes

  2. Referee: The central derivation (that the biconditional produces a sound complete decidable system prohibited by Gödel) does not go through once the witness-length condition fails to hold for the full set of theorems. The manuscript provides no explicit construction or proof that the checking relation R for Gödel's predicate satisfies the bounded-witness form for all theorems.

    Authors: We agree that without the bounded-witness condition holding, the derivation for the specific case of PA theorems does not apply directly. The core of our argument is that the semantic definition of NP imposes, for every language in NP, a biconditional equating membership with the existence of a polynomially bounded witness verifiable in polynomial time. This structure mirrors a sound and complete proof system with decidable verification. For languages rich enough to interpret arithmetic, this would contradict Gödel's theorem if the language were to include all truths. We will add a clarification in the manuscript explaining that the inconsistency arises for the class of languages defined by the NP form, and we will not rely on the PA theorems being in NP. revision: yes

  3. Referee: The argument invokes the semantic definition of NP without addressing that standard accounts place the set of true arithmetic sentences outside NP precisely because of the absence of a uniform polynomial witness bound.

    Authors: The manuscript's point is not to place true arithmetic sentences in NP but to examine what the definition entails for those languages that do meet the criteria. By requiring the biconditional with bounded witnesses, the definition effectively asserts that truth coincides with the existence of short verifiable proofs for member languages. We will revise the text to explicitly contrast this with the known status of arithmetic truths and to explain why the definition still leads to the identified tension with incompleteness results for the languages it does classify. revision: yes

standing simulated objections not resolved
  • We cannot provide an explicit construction showing that Gödel's predicate satisfies the NP witness bound for PA theorems, as no such bound exists.

Circularity Check

0 steps flagged

No significant circularity; argument rests on external theorems

full rationale

The paper derives its claim by interpreting the standard NP definition (poly-time R plus fixed-k witness bound) as instantiating a sound complete decidable system, then observing that Gödel's proof-checking relation satisfies the poly-time condition and therefore falls inside the definition, yielding a contradiction with incompleteness. No step reduces a derived quantity to a fitted parameter or self-citation by construction; the biconditional and the claim that the relation 'fits as a literal instance' are interpretive applications of externally established facts (Gödel 1931, Cook-Levin, standard NP definition) rather than internal redefinitions or renamings. The derivation is therefore self-contained against external benchmarks and receives the default non-circularity finding.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The argument rests on standard results from logic and the accepted definition of NP without introducing new free parameters or postulated entities; the load-bearing assumptions are the interpretation of the membership biconditional as a complete proof system and the claim that Gödel's checker satisfies the polynomial witness bound.

axioms (3)
  • standard math Gödel's First Incompleteness Theorem: any consistent formal system containing arithmetic is incomplete
    Invoked to prohibit the existence of a sound, complete, decidable proof system for all truths.
  • domain assumption The NP membership biconditional creates a sound, complete, decidable proof system for each L
    This is the paper's interpretation of the definition as instantiating Hilbert's triple.
  • domain assumption Gödel's proof-checking relation is polynomial-time and fits the bounded-witness NP form
    Claimed to be a literal instance of the checking relation R with fixed k.

pith-pipeline@v0.9.0 · 5470 in / 1731 out tokens · 92661 ms · 2026-05-10T18:00:24.853158+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

12 extracted references · 12 canonical work pages

  1. [1]

    Algebrization: A new barrier in complexity theory

    Scott Aaronson and Avi Wigderson. Algebrization: A new barrier in complexity theory. In ACM Transactions on Computation Theory, volume 1, pages 2:1–2:54, 2009

    work page 2009

  2. [2]

    Cambridge University Press, 2009

    Sanjeev Arora and Boaz Barak.Computational Complexity: A Modern Approach. Cambridge University Press, 2009

    work page 2009

  3. [3]

    Relativizations of theP= ?N Pquestion

    Theodore Baker, John Gill, and Robert Solovay. Relativizations of theP= ?N Pquestion. SIAM Journal on Computing, 4(4):431–442, 1975

    work page 1975

  4. [4]

    Stephen A. Cook. The complexity of theorem-proving procedures. InProceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC), pages 151–158. ACM, 1971

    work page 1971

  5. [5]

    Stephen A. Cook. The P versus NP problem. In James Carlson, Arthur Jaffe, and Andrew Wiles, editors,The Millennium Prize Problems, pages 87–104. American Mathematical Society and Clay Mathematics Institute, 2006

    work page 2006

  6. [6]

    Cook and Robert A

    Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof sys- tems.Journal of Symbolic Logic, 44(1):36–50, 1979

    work page 1979

  7. [7]

    ¨Uber formal unentscheidbare S¨ atze der Principia Mathematica und verwandter Systeme I.Monatshefte f¨ ur Mathematik und Physik, 38:173–198, 1931

    Kurt G¨ odel. ¨Uber formal unentscheidbare S¨ atze der Principia Mathematica und verwandter Systeme I.Monatshefte f¨ ur Mathematik und Physik, 38:173–198, 1931. English translation in [12]

    work page 1931

  8. [8]

    Cambridge University Press, 2019

    Jan Kraj´ ıˇ cek.Proof Complexity, volume 170 ofEncyclopedia of Mathematics and its Applica- tions. Cambridge University Press, 2019

    work page 2019

  9. [9]

    Some consequences of cryptographical conjectures forS1 2 and EF.Information and Computation, 140(1):82–94, 1998

    Jan Kraj´ ıˇ cek and Pavel Pudl´ ak. Some consequences of cryptographical conjectures forS1 2 and EF.Information and Computation, 140(1):82–94, 1998

    work page 1998

  10. [10]

    On the length of proofs of finitistic consistency statements in first-order theories

    Pavel Pudl´ ak. On the length of proofs of finitistic consistency statements in first-order theories. InLogic Colloquium ’84, pages 165–196. North-Holland, 1986

    work page 1986

  11. [11]

    Razborov and Steven Rudich

    Alexander A. Razborov and Steven Rudich. Natural proofs.Journal of Computer and System Sciences, 55(1):24–35, 1997

    work page 1997

  12. [12]

    Harvard University Press, 1967

    Jean van Heijenoort, editor.From Frege to G¨ odel: A Source Book in Mathematical Logic, 1879–1931. Harvard University Press, 1967. 8

    work page 1931