On some generalizations of G\"{o}del's second incompleteness theorem

Keita Yokoyama; Yudai Suzuki

arxiv: 2606.29802 · v1 · pith:EHHXNDZPnew · submitted 2026-06-29 · 🧮 math.LO

On some generalizations of G\"{o}del's second incompleteness theorem

Yudai Suzuki , Keita Yokoyama This is my paper

Pith reviewed 2026-06-30 04:17 UTC · model grok-4.3

classification 🧮 math.LO

keywords Gödel's second incompleteness theoremω-modelβ_n-modelCraig's trickreverse mathematicsinduction axiomsdefinable complexitysemantic incompleteness

0 comments

The pith

Gödel's second incompleteness theorem extends to the unprovability of ω-models and β_n-models of a theory via a unified proof.

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

The paper revisits Gödel's second incompleteness theorem through two lenses. The first connects the definable complexity of a theory to the unprovability of its own soundness and shows how induction axioms mediate this link while measuring the reverse-mathematical strength of Craig's trick. The second treats the theorem as the unprovability of a model's existence and replaces ordinary models with ω-models or β_n-models. A single new argument covers both of these semantic variants. Together the results tighten the boundary on what a theory can formally assert about its own consistency and models.

Core claim

We give some generalizations of Gödel's second incompleteness theorem and study their surroundings. We revisit it from two perspectives. One perspective is the relationship between the definable complexity of a theory and unprovability of its soundness. We clarify the relationship between this perspective and induction axioms. We also determine the logical strength of Craig's trick, which is important for studying the definability of a theory, from the point of view of reverse mathematics. The other perspective is semantic incompleteness. The second incompleteness theorem may be seen as the unprovability of the existence of a model. It is known that 'model' is replaced with 'ω-model' or 'β_n

What carries the argument

The definable-complexity/soundness link mediated by induction axioms together with the semantic substitution of ω-models or β_n-models for ordinary models.

If this is right

A theory cannot prove its own soundness when its definable complexity is constrained by the induction axioms it satisfies.
Craig's trick has a precise strength in the hierarchy of reverse-mathematical systems.
No theory proves the existence of an ω-model of itself under the conditions of the unified argument.
No theory proves the existence of a β_n-model of itself under the conditions of the unified argument.

Where Pith is reading between the lines

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

The two perspectives may be combined to obtain joint bounds on both syntactic consistency statements and semantic model existence.
The results suggest that similar substitutions (e.g., to other classes of models) could be handled by modest adjustments to the unified proof.
The reverse-mathematical calibration of Craig's trick supplies a concrete yardstick for comparing definability restrictions across different base systems.

Load-bearing premise

The definable complexity of a theory is related to the unprovability of its soundness through induction axioms.

What would settle it

A consistent theory whose definable complexity is low enough to fall under the first perspective yet which still proves the existence of one of its own ω-models.

read the original abstract

In this note, we give some generalizations of G\"{o}del's second incompleteness theorem and study their surroundings. We revisit it from two perspectives. One perspective is the relationship between the definable complexity of a theory and unprovability of its soundness. We clarify the relationship between this perspective and induction axioms. We also determine the logical strength of Craig's trick, which is important for studying the definability of a theory, from the point of view of reverse mathematics. The other perspective is semantic incompleteness. The second incompleteness theorem may be seen as the unprovability of the existence of a model. It is known that `model' is replaced with `$\omega$-model' or `$\beta_n$-model'. We give a new and unified proof of the $\omega$-model and $\beta_n$-model versions of the incompleteness theorem.

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.

Desk Editor's Note private letter to a colleague

This note gives a unified proof of the ω-model and β_n-model versions of Gödel's second incompleteness theorem along with reverse-math results on Craig's trick.

read the letter

The main thing here is a new unified proof for the ω-model and β_n-model versions of the second incompleteness theorem, plus a reverse-math calculation of the strength of Craig's trick and a clarification of how definable complexity connects to the unprovability of soundness through induction axioms.

The paper organizes the two perspectives cleanly. The definability side ties the complexity of a theory to whether its soundness is provable, and shows where induction axioms matter. The semantic side treats incompleteness as failure to prove a model exists, then replaces ordinary models with ω-models or β_n-models. They present both as following from one construction, which avoids separate arguments for each case. The Craig's trick analysis is a useful side result because that device shows up often when definability is at issue.

Soft spots are minor. The abstract gives no proof sketches, so it is hard to judge exactly how much the unification saves compared with handling the cases one at a time. The link between definable complexity and soundness unprovability is taken as the basis for the first perspective rather than derived, but the paper flags it openly. The stress-test note found no internal gaps in the argument structure, so the linkages appear to hold.

This is for readers already working in proof theory and reverse mathematics who care about model existence in weak systems. Someone studying generalizations of incompleteness or the role of induction in definability would get concrete value from the organization. It is too specialized for a general logic audience.

I would send it to peer review. The claims are specific enough for referees to check the proofs directly, and the reverse-math result on Craig's trick is the sort of thing that can be verified or corrected without rewriting the whole note.

Referee Report

0 major / 2 minor

Summary. The manuscript revisits Gödel's second incompleteness theorem from two perspectives. The first examines the link between definable complexity of a theory and unprovability of its soundness, clarifies the role of induction axioms, and determines the logical strength of Craig's trick in reverse mathematics. The second perspective treats the theorem as unprovability of model existence and supplies a new unified proof of the ω-model and β_n-model versions.

Significance. If the derivations hold, the unified construction for the model-theoretic variants and the reverse-mathematics analysis of Craig's trick and induction would strengthen the technical toolkit for studying incompleteness in subsystems of second-order arithmetic, particularly by separating definability from semantic considerations.

minor comments (2)

§2: the statement of the main theorem on the logical strength of Craig's trick would benefit from an explicit comparison table with known results in RCA0 and WKL0.
The proof sketch for the unified ω-model / β_n-model result (around the common construction) leaves the handling of the induction axioms implicit; a short paragraph spelling out the exact axiom schema used would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful summary of our manuscript and the recommendation of minor revision. No specific major comments were listed in the report.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper presents a new unified proof of the ω-model and β_n-model versions of Gödel's second incompleteness theorem, along with analysis of definable complexity, soundness, induction axioms, and Craig's trick in reverse mathematics. The derivation separates definability and semantic perspectives without any reduction of claims to self-definitions, fitted parameters renamed as predictions, or load-bearing self-citations; the central construction follows from standard logical relationships and induction axioms invoked explicitly as clarifying tools rather than unexamined premises. No equations or steps in the provided abstract or description exhibit equivalence by construction to inputs, and the work rests on externally verifiable reverse-mathematics techniques.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based solely on the abstract; no free parameters, axioms, or invented entities are identifiable from the provided text.

pith-pipeline@v0.9.1-grok · 5678 in / 1061 out tokens · 52642 ms · 2026-06-30T04:17:18.362342+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

12 extracted references · 1 canonical work pages

[1]

G¨ odel’s second incomplet eness theorem for Σ n-deﬁnable theories

Conden Chao and Payam Seraji. G¨ odel’s second incomplet eness theorem for Σ n-deﬁnable theories. Log. J. IGPL , 26(2):255–257, 2018

2018
[2]

A note on fragments of uniform reﬂec tion in second order arithmetic

Emanuele Frittaion. A note on fragments of uniform reﬂec tion in second order arithmetic. Bull. Symb. Log., 28(3):451–465, 2022

2022
[3]

Generalizations o f G¨ odel’s incompleteness theorems for Σ n- deﬁnable theories of arithmetic

Makoto Kikuchi and Taishi Kurahashi. Generalizations o f G¨ odel’s incompleteness theorems for Σ n- deﬁnable theories of arithmetic. Rev. Symb. Log. , 10(4):603–616, 2017

2017
[4]

Incompleteness and jump hi erarchies

Patrick Lutz and James Walsh. Incompleteness and jump hi erarchies. Proc. Am. Math. Soc. , 148(11):4997–5006, 2020

2020
[5]

Incomplet eness and jump hierarchies

Patrick Lutz and James Walsh. Corrigenda to: “Incomplet eness and jump hierarchies”. Proc. Am. Math. Soc. , 149(7):3143–3144, 2021

2021
[6]

Carl Mummert and Stephen G. Simpson. An incompleteness t heorem for β n-models. J. Symb. Log. , 69(2):612–616, 2004

2004
[7]

“natural” representations and extensions of G¨ odel’s second theorem

Karl-Georg Niebergall. “natural” representations and extensions of G¨ odel’s second theorem. In Logic colloquium ’01. Proceedings of the annual European summer m eeting of the Association for Symbolic Logic (ASL), Vienna, Austria, August 6–11, 2001 , pages 350–368. Wellesley, MA: A K Peters; Urbana, IL: Association for Symbolic Logic, 2005

2001
[8]

Stephen G. Simpson. Subsystems of second order arithmetic . Perspect. Log. Cambridge: Cambridge University Press; Urbana, IL: Association for Symbolic Log ic (ASL), paperback reprint of the 2nd ed. 2009 edition, 2010

2009
[9]

Descending sequences of degrees

John Steel. Descending sequences of degrees. J. Symb. Log. , 40:59–61, 1975

1975
[10]

Searching problems ab ove arithmetical transﬁnite recursion

Yudai Suzuki and Keita Yokoyama. Searching problems ab ove arithmetical transﬁnite recursion. Ann. Pure Appl. Logic , 175(10):31, 2024. Id/No 103488

2024
[11]

A classiﬁcation of incom pleteness statements

Henry Towsner and James Walsh. A classiﬁcation of incom pleteness statements. Preprint, arXiv:2409.05973 [math.LO] (2025), 2025

work page arXiv 2025
[12]

An incompleteness theorem via ordinal ana lysis

James Walsh. An incompleteness theorem via ordinal ana lysis. J. Symb. Log. , 89(1):80–96, 2024. National Institute of Technology, Oyama College, Nakakuki 771, Oyama, Tochigi, Japan Email address : yudai.suzuki.research@gmail.com Mathematical Institute, Tohoku University, Aramaki Aza-A oba 6-3, Aoba-ku, Sendai, Miyagi, Japan Email address : keita.yokoyama...

2024

[1] [1]

G¨ odel’s second incomplet eness theorem for Σ n-deﬁnable theories

Conden Chao and Payam Seraji. G¨ odel’s second incomplet eness theorem for Σ n-deﬁnable theories. Log. J. IGPL , 26(2):255–257, 2018

2018

[2] [2]

A note on fragments of uniform reﬂec tion in second order arithmetic

Emanuele Frittaion. A note on fragments of uniform reﬂec tion in second order arithmetic. Bull. Symb. Log., 28(3):451–465, 2022

2022

[3] [3]

Generalizations o f G¨ odel’s incompleteness theorems for Σ n- deﬁnable theories of arithmetic

Makoto Kikuchi and Taishi Kurahashi. Generalizations o f G¨ odel’s incompleteness theorems for Σ n- deﬁnable theories of arithmetic. Rev. Symb. Log. , 10(4):603–616, 2017

2017

[4] [4]

Incompleteness and jump hi erarchies

Patrick Lutz and James Walsh. Incompleteness and jump hi erarchies. Proc. Am. Math. Soc. , 148(11):4997–5006, 2020

2020

[5] [5]

Incomplet eness and jump hierarchies

Patrick Lutz and James Walsh. Corrigenda to: “Incomplet eness and jump hierarchies”. Proc. Am. Math. Soc. , 149(7):3143–3144, 2021

2021

[6] [6]

Carl Mummert and Stephen G. Simpson. An incompleteness t heorem for β n-models. J. Symb. Log. , 69(2):612–616, 2004

2004

[7] [7]

“natural” representations and extensions of G¨ odel’s second theorem

Karl-Georg Niebergall. “natural” representations and extensions of G¨ odel’s second theorem. In Logic colloquium ’01. Proceedings of the annual European summer m eeting of the Association for Symbolic Logic (ASL), Vienna, Austria, August 6–11, 2001 , pages 350–368. Wellesley, MA: A K Peters; Urbana, IL: Association for Symbolic Logic, 2005

2001

[8] [8]

Stephen G. Simpson. Subsystems of second order arithmetic . Perspect. Log. Cambridge: Cambridge University Press; Urbana, IL: Association for Symbolic Log ic (ASL), paperback reprint of the 2nd ed. 2009 edition, 2010

2009

[9] [9]

Descending sequences of degrees

John Steel. Descending sequences of degrees. J. Symb. Log. , 40:59–61, 1975

1975

[10] [10]

Searching problems ab ove arithmetical transﬁnite recursion

Yudai Suzuki and Keita Yokoyama. Searching problems ab ove arithmetical transﬁnite recursion. Ann. Pure Appl. Logic , 175(10):31, 2024. Id/No 103488

2024

[11] [11]

A classiﬁcation of incom pleteness statements

Henry Towsner and James Walsh. A classiﬁcation of incom pleteness statements. Preprint, arXiv:2409.05973 [math.LO] (2025), 2025

work page arXiv 2025

[12] [12]

An incompleteness theorem via ordinal ana lysis

James Walsh. An incompleteness theorem via ordinal ana lysis. J. Symb. Log. , 89(1):80–96, 2024. National Institute of Technology, Oyama College, Nakakuki 771, Oyama, Tochigi, Japan Email address : yudai.suzuki.research@gmail.com Mathematical Institute, Tohoku University, Aramaki Aza-A oba 6-3, Aoba-ku, Sendai, Miyagi, Japan Email address : keita.yokoyama...

2024