pith. sign in

arxiv: 2501.11220 · v2 · pith:UHMDSM4Cnew · submitted 2025-01-20 · 🧮 math.LO

Proof-theoretic dilator and intermediate pointclasses

Hanul Jeon This is my paper

Pith reviewed 2026-05-23 05:46 UTC · model grok-4.3

classification 🧮 math.LO
keywords proof theorydilatorsintermediate pointclassesSpector classesordinal analysisΣ¹₂ analysisΠ¹₂ proof theorygeneralized ordinal analysis
0
0 comments X

The pith

Dilators and intermediate pointclasses connect through Σ¹₂ analysis.

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

The paper shows that two generalizations of ordinal analysis are linked in a direct way. Girard's approach assigns dilators to theories in a Π¹₂ setting, while the other uses Spector classes to reach ordinals beyond the Church-Kleene ordinal. The author argues that Σ¹₂-proof theoretic analysis supplies the bridge that makes these two assignments systematically correspond. A reader would care because the link suggests that proof-theoretic strength can be measured in either language once the connection is in place.

Core claim

Dilators and intermediate pointclasses are systematically entangled, and Σ¹₂-proof theoretic analysis has a critical role in connecting the dilator-based generalization of ordinal analysis with the Spector-class generalization.

What carries the argument

The direct correspondence between dilators and intermediate pointclasses that is mediated by Σ¹₂ objects.

If this is right

  • Results proved with dilators can be restated as results about intermediate pointclasses and conversely.
  • Σ¹₂ analysis becomes the common language for comparing the two frameworks.
  • The strength of a theory can be read indifferently from its dilator or from its Spector class once the correspondence is fixed.
  • Generalized ordinal analyses gain a single underlying scale rather than two separate ones.

Where Pith is reading between the lines

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

  • The unification may let researchers move a consistency proof from one setting to the other without rebuilding the argument.
  • The same bridge could be tested on stronger pointclasses or on dilators of higher type.
  • Questions about the computational content of theories might be rephrased as questions about the pointclass side of the correspondence.
  • A mismatch for a specific theory such as Kripke-Platek set theory would isolate where the claimed entanglement breaks.

Load-bearing premise

The technical definitions of dilators and of Spector classes admit a systematic one-to-one link through Σ¹₂ objects.

What would settle it

A concrete theory whose assigned dilator fails to determine the corresponding intermediate pointclass (or vice versa) when the Σ¹₂ bridge is applied.

read the original abstract

There are two major generalizations of the standard ordinal analysis: One is Girard's $\Pi^1_2$-proof theory in which dilators are assigned to theories instead of ordinals. The other is Pohlers' generalized ordinal analysis with Spector classes, where ordinals greater than $\omega_1^{\mathsf{CK}}$ are assigned to theories. In this paper, we show that these two are systematically entangled, and $\Sigma^1_2$-proof theoretic analysis has a critical role in connecting these two.

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

0 major / 1 minor

Summary. The paper claims that Girard's dilators (from Π¹₂-proof theory) and Pohlers' Spector classes (from generalized ordinal analysis) are systematically entangled, with Σ¹₂-proof theoretic analysis playing a critical mediating role between the two frameworks.

Significance. If the claimed entanglement is established with explicit constructions, it would link two distinct generalizations of ordinal analysis, potentially allowing transfer of results between dilator assignments and Spector-class assignments via Σ¹₂ objects and thereby unifying aspects of proof-theoretic strength measures.

minor comments (1)
  1. The provided text consists only of the abstract; the manuscript should include explicit definitions, constructions, and at least one worked example (e.g., for a specific theory such as ATR₀ or KP) showing how a dilator corresponds to a Spector class via a Σ¹₂ object.

Simulated Author's Rebuttal

0 responses · 0 unresolved

Thank you for the opportunity to respond to the referee report on our manuscript. The referee's summary accurately captures the main claim of the paper regarding the entanglement between dilator-based and Spector-class generalizations of ordinal analysis via Σ¹₂-proof theory. However, no specific major comments are listed in the report. Consequently, we do not have point-by-point responses. We would welcome any specific questions or suggestions from the referee to improve the manuscript.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The manuscript abstract and surrounding context state a high-level result that Girard's dilators and Pohlers' Spector classes are systematically entangled via Σ¹₂-proof theoretic analysis, but supply no equations, explicit definitions, derivation steps, or self-citations that could be examined for reduction to inputs by construction. No load-bearing claim is visible that equates a derived quantity to a fitted parameter or prior self-referential result, so the derivation chain cannot be shown to collapse internally.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract supplies no explicit free parameters, axioms, or invented entities; ledger left empty due to lack of technical content.

pith-pipeline@v0.9.0 · 5595 in / 943 out tokens · 21094 ms · 2026-05-23T05:46:58.014298+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

32 extracted references · 32 canonical work pages

  1. [1]

    The Π1 2 consequences of a theory

    J. P. Aguilera and F. Pakhomov. “The Π1 2 consequences of a theory”. In: J. Lond. Math. Soc. (2) 107.3 (2023), pp. 1045–1073

    work page 2023

  2. [2]

    Π1 2 proof-theoretic analysis

    J. P. Aguilera and F. Pakhomov. “ Π1 2 proof-theoretic analysis.” In preperation

    work page

  3. [3]

    Non-linearities in the a nalytical hierarchy

    J. P. Aguilera and F. Pakhomov. “Non-linearities in the a nalytical hierarchy”. Preprint. url: https:// www.dropbox.com/scl/fi/2i2e7x9yfyl9f0jmloowg/NonLinearities.pdf

    work page

  4. [4]

    Boundedness theorems for flowers an d sharps

    J. P. Aguilera et al. “Boundedness theorems for flowers an d sharps”. In: Proc. Amer. Math. Soc. 150.9 (2022), pp. 3973–3988

    work page 2022

  5. [5]

    Well ordering principles and Π1 4-statements: a pilot study

    Anton Freund. “Well ordering principles and Π1 4-statements: a pilot study”. In: J. Symb. Log. 86.2 (2021), pp. 709–745

    work page 2021

  6. [6]

    Π1 2-logic. I. Dilators

    Jean-Yves Girard. “ Π1 2-logic. I. Dilators”. In: Ann. Math. Logic 21.2-3 (1981), pp. 75–219

    work page 1981

  7. [7]

    Introduction to Π1 2-Logic

    Jean-Yves Girard. “Introduction to Π1 2-Logic”. In: Synthese 62.2 (1985), pp. 191–216

    work page 1985

  8. [8]

    Proof theory and logical complexity

    Jean-Yves Girard. Proof theory and logical complexity . Vol. 1. Studies in Proof Theory. Monographs. Bibliopolis, Naples, 1987, p. 505

    work page 1987

  9. [9]

    Proof theory and logical complexity II

    Jean-Yves Girard. “Proof theory and logical complexity II”. Unpublished manuscript. url: https:// girard.perso.math.cnrs.fr/ptlc2.pdf

    work page

  10. [10]

    Embeddability of pt ykes

    Jean-Yves Girard and Dag Normann. “Embeddability of pt ykes”. In: J. Symbolic Logic 57.2 (1992), pp. 659–676

    work page 1992

  11. [11]

    Eléments de logique Π1 n

    Jean-Yves Girard and Jean-Pierre Ressayre. “Eléments de logique Π1 n”. In: Recursion theory (Ithaca, N.Y., 1982). Vol. 42. Proc. Sympos. Pure Math. Amer. Math. Soc., Provide nce, RI, 1985, pp. 389–445

    work page 1982

  12. [12]

    Peter G. Hinman. Recursion-theoretic hierarchies. Perspectives in Mathematical Logic. Springer-Verlag, Berlin-New York, 1978. 46 REFERENCES

    work page 1978

  13. [13]

    The behavior of Higher proof theory I: Case Σ1

    Hanul Jeon. The behavior of Higher proof theory I: Case Σ1

    work page

  14. [14]

    arXiv: 2406.03801

    2024. arXiv: 2406.03801

    work page arXiv 2024

  15. [15]

    Moschovakis

    Yiannis N. Moschovakis. Elementary induction on abstract structures . Vol. Vol. 77. Studies in Logic and the Foundations of Mathematics. North-Holland Publish ing Co., Amsterdam-London; American Elsevier Publishing Co., Inc., New York, 1974

    work page 1974

  16. [16]

    Moschovakis

    Yiannis N. Moschovakis. Descriptive set theory . Second. Vol. 155. Mathematical Surveys and Mono- graphs. American Mathematical Society, Providence, RI, 20 09

    work page

  17. [17]

    Reducing ω -model reflection to iterated syntactic reflection

    Fedor Pakhomov and James Walsh. “Reducing ω -model reflection to iterated syntactic reflection”. In: Journal of Mathematical Logic 23.02 (2023), p. 2250001. doi: 10.1142/S0219061322500015

    work page doi:10.1142/s0219061322500015 2023

  18. [18]

    Proof theory

    Wolfram Pohlers. Proof theory. Universitext. The first step into impredicativity. Spring er-Verlag, Berlin, 2009

    work page 2009

  19. [19]

    Semi-formal calculi and their appli cations

    Wolfram Pohlers. “Semi-formal calculi and their appli cations”. In: Gentzen’s centenary. Springer, Cham, 2015, pp. 317–354. isbn: 978-3-319-10102-6; 978-3-319-10103-3

    work page 2015

  20. [20]

    Iterated inductive definitions revi sited

    Wolfram Pohlers. “Iterated inductive definitions revi sited”. In: Feferman on foundations. Vol. 13. Outst. Contrib. Log. Springer, Cham, 2017, pp. 209–251

    work page 2017

  21. [21]

    On the performance of axiom systems

    Wolfram Pohlers. “On the performance of axiom systems” . In: Axiomatic Thinking. II . Springer, Cham, 2022, pp. 35–88

    work page 2022

  22. [22]

    The role of parameters in bar rule and bar induction

    Michael Rathjen. “The role of parameters in bar rule and bar induction”. In: J. Symbolic Logic 56.2 (1991), pp. 715–730

    work page 1991

  23. [23]

    The realm of ordinal analysis

    Michael Rathjen. “The realm of ordinal analysis”. In: London Mathematical Society Lecture Note Series (1999), pp. 219–280

    work page 1999

  24. [24]

    Recursively Mahlo ordinals and induct ive definitions

    Wayne Richter. “Recursively Mahlo ordinals and induct ive definitions”. In: Logic Colloquium ’69 (Proc. Summer School and Colloq., Manchester, 1969) . Vol. 61. Stud. Logic Found. Math. North-Holland, Amsterdam-London, 1971, pp. 273–288

    work page 1969

  25. [25]

    Inductive definitions a nd reflecting properties of admissible ordinals

    Wayne Richter and Peter Aczel. “Inductive definitions a nd reflecting properties of admissible ordinals”. In: Generalized recursion theory (Proc. Sympos., Univ. Oslo, Osl o, 1972) . Vol. 79. Stud. Logic Found. Math. North-Holland, Amsterdam-London, 1974, pp. 301–381

    work page 1972

  26. [26]

    Higher Recursion Theory

    Gerald E Sacks. Higher Recursion Theory . Vol. 2. Cambridge University Press, 2017

    work page 2017

  27. [27]

    Stephen G. Simpson. Subsystems of second order arithmetic . Vol. 1. Cambridge University Press, 2009

    work page 2009

  28. [28]

    A complete classification of the ∆1 2-functions

    Yoshindo Suzuki. “A complete classification of the ∆1 2-functions”. In: Bull. Amer. Math. Soc. 70 (1964), pp. 246–253

    work page 1964

  29. [29]

    A classification of incompleteness statements

    Henry Towsner and James Walsh. A classification of incompleteness statements . 2024. arXiv: 2409.05973

    work page arXiv 2024

  30. [30]

    Cut-elimination and interpo lation of Ω-logic

    Jacqueline Vauzeilles. “Cut-elimination and interpo lation of Ω-logic”. In: Arch. Math. Logic 27.2 (1988), pp. 161–175. issn: 0933-5846,1432-0665. doi: 10.1007/BF01620764. url: https://doi.org/10.1007/ BF01620764

    work page doi:10.1007/bf01620764 1988

  31. [31]

    An incompleteness theorem via ordinal an alysis

    James Walsh. “An incompleteness theorem via ordinal an alysis”. In: The Journal of Symbolic Logic (2022), pp. 1–17

    work page 2022

  32. [32]

    Characterizations of ordinal analysis

    James Walsh. “Characterizations of ordinal analysis” . In: Annals of Pure and Applied Logic 174.4 (2023), p. 103230. Email address : hj344@cornell.edu URL: https://hanuljeon95.github.io Department of Mathematics, Cornell University, Ithaca, NY 14853

    work page 2023