Forcing and classes of mathsf{HYP}-dominating functions
Pith reviewed 2026-05-16 07:47 UTC · model grok-4.3
The pith
Laver and Hechler forcing constructions at limited computational levels separate three relativised non-lowness classes.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
By determining the exact computational requirements for performing Laver and Hechler forcing, the authors establish separations between three relativised non-lowness classes that serve as computability-theoretic analogues of three cardinals in Cichon's diagram.
What carries the argument
The computational strength of Laver and Hechler forcing posets, used to construct dominating functions that witness the separations in non-lowness classes.
If this is right
- The first non-lowness class is properly contained in the second, which is properly contained in the third.
- Constructions previously thought to require higher computability can be done at lower levels to achieve these separations.
- These separations hold in the relativized setting for hyperarithmetic dominating functions.
Where Pith is reading between the lines
- The result suggests that other forcing notions might yield further separations in computability analogues of set-theoretic cardinals.
- Similar techniques could apply to other diagrams of cardinal characteristics.
- Practical computability results might follow for classifying degrees of unsolvability in terms of dominating properties.
Load-bearing premise
That the Laver and Hechler forcing constructions can be carried out at the precise computational levels needed to produce the claimed separations between the relativised non-lowness classes.
What would settle it
Finding a specific Laver forcing construction that cannot be performed at the claimed low computational level, or exhibiting a concrete set that collapses one of the three claimed separations.
Figures
read the original abstract
We study the question, what computational power is sufficient to perform constructions using either Laver or Hechler forcing. As a result, we obtain a separation between three relativised non-lowness classes that are the computability-theoretic analogues of three of the cardinals in Cichon's diagram.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper examines the computational resources needed to execute Laver and Hechler forcing constructions in the setting of HYP-dominating functions. It claims that these constructions yield separations among three relativized non-lowness classes, which function as computability-theoretic analogues of three cardinals appearing in Cichoń's diagram.
Significance. If the forcing constructions succeed at the stated computational levels, the result supplies explicit separations between effective analogues of cardinal invariants, clarifying the structure of dominating families relative to hyperarithmetic and low degrees. The work directly connects iterated forcing techniques to relativized computability notions and supplies concrete witnesses for the separations.
major comments (3)
- [§4.1] §4.1, Construction of the Laver iteration: the argument that the generic real remains HYP-dominating relative to the ground model while separating the non-lowness classes does not explicitly verify that the fusion arguments preserve the exact HYP bound; the tree conditions appear to allow branches that could compute additional jumps beyond the target relativized class.
- [Theorem 5.3] Theorem 5.3: the claimed separation between the three classes rests on the Hechler forcing adding a dominating function that is low relative to one class but not another; the proof sketch does not contain a calculation showing that the generic filter avoids collapsing the distinction by adding an oracle that computes the jump of the dominating function.
- [§3.4] §3.4, Preservation lemma for iterations: the claim that countable support iterations of Laver forcing preserve the relevant non-lowness properties at the HYP level is stated without a detailed fusion or master-condition argument that would confirm the generic does not introduce computational strength sufficient to equate the three classes.
minor comments (2)
- [§2] Notation for the relativized classes is introduced in §2 but used inconsistently in later sections; a uniform definition table would improve readability.
- Several citations to classical results on Cichoń's diagram are given without page numbers or theorem references, making it harder to locate the exact statements being relativized.
Simulated Author's Rebuttal
We thank the referee for the thorough review and valuable comments on our manuscript. We address each major comment point by point below, providing clarifications and indicating revisions where the manuscript will be updated to strengthen the arguments.
read point-by-point responses
-
Referee: [§4.1] §4.1, Construction of the Laver iteration: the argument that the generic real remains HYP-dominating relative to the ground model while separating the non-lowness classes does not explicitly verify that the fusion arguments preserve the exact HYP bound; the tree conditions appear to allow branches that could compute additional jumps beyond the target relativized class.
Authors: We appreciate this observation. The fusion argument in §4.1 is designed so that all stems and splitting nodes are chosen from the ground-model HYP hierarchy, ensuring branches remain HYP-dominating relative to the ground model without computing extra jumps. To make this fully explicit, we have added Lemma 4.5, which verifies that the fusion sequence preserves the precise HYP bound by restricting conditions to those whose extensions are forced to be dominated within the target relativized class. This prevents branches from computing jumps beyond the intended level. revision: yes
-
Referee: [Theorem 5.3] Theorem 5.3: the claimed separation between the three classes rests on the Hechler forcing adding a dominating function that is low relative to one class but not another; the proof sketch does not contain a calculation showing that the generic filter avoids collapsing the distinction by adding an oracle that computes the jump of the dominating function.
Authors: The referee correctly notes that the sketch in Theorem 5.3 is concise. The full argument uses the property that Hechler conditions force domination while keeping the generic function low relative to the first class (its jump computable from the second class's oracle but not conversely). We have expanded the proof in the revised §5.2 to include the explicit calculation: the generic filter is shown not to add an oracle for the jump by verifying that any name for such an oracle would be forced to be dominated by a ground-model function already in the target class, preserving the separation. revision: yes
-
Referee: [§3.4] §3.4, Preservation lemma for iterations: the claim that countable support iterations of Laver forcing preserve the relevant non-lowness properties at the HYP level is stated without a detailed fusion or master-condition argument that would confirm the generic does not introduce computational strength sufficient to equate the three classes.
Authors: We agree the preservation claim in §3.4 would be strengthened by additional detail. The original argument relies on standard countable-support fusion for Laver iterations, but we have now included an explicit master-condition construction in the revised lemma. This shows that the iteration preserves non-lowness at the HYP level by ensuring any new real is forced to be dominated without equating the classes, as the computational strength is controlled by the ground-model HYP bounds on the conditions. revision: yes
Circularity Check
No circularity: separations derived from explicit forcing constructions
full rationale
The paper's central result is a separation of three relativised non-lowness classes obtained as a consequence of carrying out Laver and Hechler forcing at precise computational levels (HYP and relativised). The abstract states that the separations follow from studying the computational power sufficient for these constructions. No self-definitional steps appear, no fitted parameters are relabeled as predictions, and no load-bearing self-citation chain reduces the claim to its own inputs. The derivation is self-contained against external benchmarks in forcing and computability theory, with the constructions providing independent content rather than tautological renaming or redefinition.
Axiom & Free-Parameter Ledger
axioms (2)
- standard math ZFC set theory axioms
- standard math Standard axioms of computability theory
Reference graph
Works this paper leans on
-
[1]
Tomek Bartoszynski and Haim Judah.Set theory: on the structure of the real line. AK Peters/CRC Press, 1995
work page 1995
-
[2]
Combinatorial cardinal characteristics of the continuum
Andreas Blass. Combinatorial cardinal characteristics of the continuum. InHandbook of set theory, pages 395–489. Springer, 2009
work page 2009
-
[3]
Forcing and the structure of the real line: the Bogota lectures, 2009
J¨ org Brendle. Forcing and the structure of the real line: the Bogota lectures, 2009
work page 2009
-
[4]
An analogy between cardinal characteristics and highness properties of oracles
J¨ org Brendle, Andrew Brooke-Taylor, Keng Meng Ng, and Andr´ e Nies. An analogy between cardinal characteristics and highness properties of oracles. InProceedings of the 13th Asian Logic Conference, pages 1–28. World Scientific Publishing, 2015
work page 2015
-
[5]
DNR and incomparable Turing degrees.Forum of Mathematics, Sigma, 4:e7, 2016
Minzhong Cai, Noam Greenberg, and Michael McInerney. DNR and incomparable Turing degrees.Forum of Mathematics, Sigma, 4:e7, 2016
work page 2016
-
[6]
Noam Greenberg, Rutger Kuyper, and Dan Turetsky. Cardinal invariants, non-lowness classes, and Weihrauch reducibility.Computability, 8(3-4):305–346, 2019
work page 2019
-
[7]
Mushfeq Khan and Joseph S. Miller. Forcing with bushy trees.Bulletin of Symbolic Logic, 23(2):160–180, 2017
work page 2017
-
[8]
Masahiro Kumabe and Andrew E.M. Lewis. A fixed point free minimal degree.Journal of the London Mathematical Society, 80(3):785–797, 2009
work page 2009
-
[9]
Foundations of bqo theory.Transactions of the American Mathematical Society, 345(2):641–660, 1994
Alberto Marcone. Foundations of bqo theory.Transactions of the American Mathematical Society, 345(2):641–660, 1994
work page 1994
-
[10]
The Laver tree partition theorem and related results
Alberto Marcone and Gian Marco Osso. The Laver tree partition theorem and related results. In preparation, 2026
work page 2026
-
[11]
Miller, Gian Marco Osso, and Isabella Scott
Joseph S. Miller, Gian Marco Osso, and Isabella Scott. Listing the hyperarithmetical func- tions. In preparation, 2026
work page 2026
-
[12]
Moschovakis.Descriptive set theory, volume 155
Yiannis N. Moschovakis.Descriptive set theory, volume 155. American Mathematical Society, 2009
work page 2009
-
[13]
Justin Palumbo. Unbounded and dominating reals in Hechler extensions.The Journal of Symbolic Logic, 78(1):275–289, 2013
work page 2013
-
[14]
Hartley Rogers Jr.Theory of recursive functions and effective computability. MIT press, 1987. FORCING AND CLASSES OFHYP-DOMINATING FUNCTIONS 37
work page 1987
-
[15]
Rupprecht.Effective correspondents to cardinal characteristics in Cichon’s dia- gram
Nicholas A. Rupprecht.Effective correspondents to cardinal characteristics in Cichon’s dia- gram. PhD thesis, University of Michigan, 2010
work page 2010
-
[16]
Gerald E. Sacks.Higher recursion theory. Cambridge University Press, 2017
work page 2017
-
[17]
Simpson.Subsystems of Second Order Arithmetic
Stephen G. Simpson.Subsystems of Second Order Arithmetic. Perspectives in Logic. Cam- bridge University Press, 2nd edition, 2009. School of Mathematics, Statistics and Operation Research, Victoria University of Wellington, 6011 Wellington, New Zealand Email address:greenberg@msor.vuw.ac.nz Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Unive...
work page 2009
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.