pith. sign in

arxiv: 2605.21175 · v1 · pith:MRIWB7ARnew · submitted 2026-05-20 · 🧮 math.LO

Forcing Sigma¹₁-Separation on ω₁^(ω₁)

Stefan Hoffelner This is my paper

Pith reviewed 2026-05-21 01:34 UTC · model grok-4.3

classification 🧮 math.LO
keywords forcingconsistencySigma11 separationDelta11 setsomega1^omega1continuum hypothesisdescriptive set theoryconstructible universe
0
0 comments X

The pith

It is consistent that any two disjoint boldface Σ¹₁ subsets of ω₁^ω₁ can be separated by a boldface Δ¹₁ set.

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

The paper establishes the consistency of a separation principle for boldface analytic sets on the space of functions from ω₁ to ω₁. It begins in the constructible universe L and applies a forcing extension that preserves the continuum hypothesis along with the equality ω₁^{<ω₁} = ω₁. If the result holds, classical separation for analytic sets extends to this larger domain while cardinal arithmetic remains controlled. A reader would care because the construction maps out how far such regularity properties can reach without extra axioms beyond ZFC plus CH.

Core claim

There is a forcing extension of L in which the continuum hypothesis holds and every pair of disjoint boldface Σ¹₁ subsets of ω₁^ω₁ admits a boldface Δ¹₁ set that separates them.

What carries the argument

A forcing extension of L that preserves CH and forces the boldface Σ¹₁-separation property on the space ω₁^ω₁.

If this is right

  • Any two disjoint boldface Σ¹₁ subsets of ω₁^ω₁ admit a boldface Δ¹₁ separator.
  • The separation holds in a model satisfying the continuum hypothesis.
  • The relation ω₁^{<ω₁} = ω₁ remains true after the forcing.
  • Separation principles from the classical theory of the reals extend to the space ω₁^ω₁ under CH.

Where Pith is reading between the lines

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

  • Similar forcing techniques might establish separation or other regularity properties for higher pointclasses on the same space.
  • The result raises the question of whether the separation can be obtained from assumptions weaker than starting in L.
  • It could be combined with other forcing constructions to produce models satisfying multiple generalized regularity properties at once.

Load-bearing premise

The construction begins in the constructible universe L and uses a forcing that preserves both the continuum hypothesis and the equality ω₁^{<ω₁} = ω₁.

What would settle it

A model of set theory in which two disjoint boldface Σ¹₁ subsets of ω₁^ω₁ exist with no boldface Δ¹₁ set separating them.

read the original abstract

We prove that it is consistent that every two disjoint boldface $\mathbf{\Sigma}^1_1$ subsets of $\omega_1^{\omega_1}$ can be separated by a boldface $\mathbf{\Delta}^1_1$ set. The forcing starts from $L$ and preserves CH and therefore also $\omega_1^{<\omega_1}=\omega_1$.

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

1 major / 0 minor

Summary. The paper claims to prove the consistency of the statement that every two disjoint boldface Σ¹₁ subsets of ω₁^ω₁ can be separated by a boldface Δ¹₁ set. The proof is by a forcing construction that begins in L (where GCH holds) and preserves CH, which in turn preserves ω₁^{<ω₁}=ω₁.

Significance. If the technical details of the forcing construction hold, the result would be a solid contribution to higher descriptive set theory. It shows that a natural separation property for the boldface pointclass Σ¹₁ can be forced on the space ω₁^ω₁ while keeping CH, thereby controlling the cardinality of the space and the number of pairs that must be handled by bookkeeping. The approach of starting from L and preserving CH is standard, but a successful verification would add a concrete example of how such separation properties interact with cardinal arithmetic at ω₁.

major comments (1)
  1. [Abstract] Abstract: the claim that the forcing 'preserves CH and therefore also ω₁^{<ω₁}=ω₁' is load-bearing for the central consistency result. Under CH the space ω₁^ω₁ has size ℵ₂ and there are ℵ₂ many pairs of disjoint boldface Σ¹₁ sets, so the iteration runs for ω₂ steps; the manuscript must supply an explicit argument (e.g., ω₁-distributivity of the iteration or a suitable support) showing that no new subsets of ω are added. Without this verification the preservation step cannot be checked and the cardinal-arithmetic assumptions used to enumerate the pairs may fail in the extension.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and for identifying the need for a more explicit verification of the preservation properties. We agree that this is a load-bearing claim and will revise the manuscript to include the requested details on the iteration's distributivity.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that the forcing 'preserves CH and therefore also ω₁^{<ω₁}=ω₁' is load-bearing for the central consistency result. Under CH the space ω₁^ω₁ has size ℵ₂ and there are ℵ₂ many pairs of disjoint boldface Σ¹₁ sets, so the iteration runs for ω₂ steps; the manuscript must supply an explicit argument (e.g., ω₁-distributivity of the iteration or a suitable support) showing that no new subsets of ω are added. Without this verification the preservation step cannot be checked and the cardinal-arithmetic assumptions used to enumerate the pairs may fail in the extension.

    Authors: We agree that an explicit argument is required. The forcing is constructed as a countable-support iteration of length ω₂ over L, where each iterand is a proper forcing that adds a separator for a given pair while preserving ω₁. Countable support ensures the iteration is ω₁-distributive: any descending sequence of length <ω₁ has a lower bound because the supports are countable and the iterands do not add new reals. We will add a dedicated lemma (new Lemma 3.5) proving this distributivity, together with a corollary that CH and ω₁^{<ω₁}=ω₁ are preserved. The bookkeeping enumeration of the ℵ₂ pairs therefore remains valid in the extension. These additions will appear in Section 3 and will be referenced from the abstract. revision: yes

Circularity Check

0 steps flagged

Standard forcing consistency proof; derivation self-contained

full rationale

The paper presents a forcing construction over L that preserves CH (hence ω₁^{<ω₁}=ω₁) while forcing boldface Σ¹₁-separation on ω₁^ω₁. No equations or definitions reduce the target separation property to itself by construction, no fitted parameters are relabeled as predictions, and no load-bearing step relies on a self-citation chain or imported uniqueness theorem. The argument is a direct consistency proof whose central claim is the existence of the extension, not a renaming or self-referential fit. This is the normal non-circular outcome for such forcing results.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on the standard axioms of ZFC together with the existence of a forcing poset over L that preserves CH and forces the separation property; no free parameters or new entities are introduced in the abstract.

axioms (1)
  • standard math ZFC
    Standard foundation for all forcing arguments in set theory.

pith-pipeline@v0.9.0 · 5582 in / 1027 out tokens · 59927 ms · 2026-05-21T01:34:08.721042+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

35 extracted references · 35 canonical work pages · 2 internal anchors

  1. [1]

    Proper forcing

    Uri Abraham. Proper forcing. In Matthew Foreman and Akihiro Kanamori, editors, Handbook of Set Theory, pages 333–394. Springer, Dordrecht, 2010

    work page 2010

  2. [2]

    Generalized Borel sets.arXiv preprint arXiv:2511.15663, 2025

    Claudio Agostini, Nick Chapman, Luca Motto Ros, and Beatrice Pitton. Generalized Borel sets.arXiv preprint arXiv:2511.15663, 2025

    work page arXiv 2025

  3. [3]

    Generalized Polish spaces at regular uncountable cardinals.Journal of the London Mathematical Society, 108(5):1886–1929, 2023

    Claudio Agostini, Luca Motto Ros, and Philipp Schlicht. Generalized Polish spaces at regular uncountable cardinals.Journal of the London Mathematical Society, 108(5):1886–1929, 2023

    work page 1929

  4. [4]

    Baumgartner, Leo A

    James E. Baumgartner, Leo A. Harrington, and Eugene M. Kleinberg. Adding a closed unbounded set.Journal of Symbolic Logic, 41(2):481–482, 1976

    work page 1976

  5. [5]

    A very absoluteΠ1 2-real singleton.Annals of Mathematical Logic, 23:101– 120, 1982

    René David. A very absoluteΠ1 2-real singleton.Annals of Mathematical Logic, 23:101– 120, 1982

    work page 1982

  6. [6]

    AΣ1 4 wellorder of the reals withNSω1 satu- rated.Journal of Symbolic Logic, 84(4):1466–1483, 2019

    Sy-David Friedman and Stefan Hoffelner. AΣ1 4 wellorder of the reals withNSω1 satu- rated.Journal of Symbolic Logic, 84(4):1466–1483, 2019

    work page 2019

  7. [7]

    American Mathematical Society, 2014

    Sy-David Friedman, Tapani Hyttinen, and Vadim Kulikov.Generalized Descriptive Set Theory and Classification Theory, volume 230 ofMemoirs of the American Mathemat- ical Society. American Mathematical Society, 2014. No. 1081

    work page 2014

  8. [8]

    Regularity properties on the generalized reals.Annals of Pure and Applied Logic, 167(4):408–430, 2016

    Sy-David Friedman, Yurii Khomskii, and Vadim Kulikov. Regularity properties on the generalized reals.Annals of Pure and Applied Logic, 167(4):408–430, 2016

    work page 2016

  9. [9]

    Degrees of rigidity for Souslin trees.Journal of Symbolic Logic, 74(2):423–454, 2009

    Gunter Fuchs and Joel David Hamkins. Degrees of rigidity for Souslin trees.Journal of Symbolic Logic, 74(2):423–454, 2009. 27

    work page 2009

  10. [10]

    Forcing theΠ 1 n-uniformization property.arXiv preprint arXiv:2103.11748, 2021

    Stefan Hoffelner. Forcing theΠ 1 n-uniformization property.arXiv preprint arXiv:2103.11748, 2021

    work page arXiv 2021

  11. [11]

    Stefan Hoffelner.NS ω1 saturated and∆ 1-definable.Journal of Symbolic Logic, 86(1):25–59, 2021

    work page 2021

  12. [12]

    Forcing theΣ1 3-separation property.Journal of Mathematical Logic, 22(2):2250008, 2022

    Stefan Hoffelner. Forcing theΣ1 3-separation property.Journal of Mathematical Logic, 22(2):2250008, 2022

    work page 2022

  13. [13]

    A Failure of $\Pi^1_{n+3}$-Reduction in the Presence of $\Sigma^1_{n+3}$-Separation

    Stefan Hoffelner. A failure ofΠ1 n+3-reduction in the presence ofΣ1 n+3-separation.arXiv preprint arXiv:2312.02540, 2023

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  14. [14]

    Forcing theΠ1 3-reduction property and a failure ofΠ1 3-uniformization

    Stefan Hoffelner. Forcing theΠ1 3-reduction property and a failure ofΠ1 3-uniformization. Annals of Pure and Applied Logic, 174(8):103292, 2023

    work page 2023

  15. [15]

    Forcing axioms and the uniformization-property.Annals of Pure and Applied Logic, 175(10):103466, 2024

    Stefan Hoffelner. Forcing axioms and the uniformization-property.Annals of Pure and Applied Logic, 175(10):103466, 2024

    work page 2024

  16. [16]

    Coding and∞-allowability for the local Delfino construction, 2025

    Stefan Hoffelner. Coding and∞-allowability for the local Delfino construction, 2025. Preprint

    work page 2025

  17. [17]

    Forcing upperΣ-uniformization in the presence of lowerΠ-reduction or uniformization.arXiv preprint arXiv:2511.05081, 2025

    Stefan Hoffelner. Forcing upperΣ-uniformization in the presence of lowerΠ-reduction or uniformization.arXiv preprint arXiv:2511.05081, 2025

    work page arXiv 2025

  18. [18]

    The globalΣ 1 n+2-uniformization property andBPFA.Advances in Mathematics, 470:110272, 2025

    Stefan Hoffelner. The globalΣ 1 n+2-uniformization property andBPFA.Advances in Mathematics, 470:110272, 2025

    work page 2025

  19. [19]

    On a local variant of the 12th Delfino problem, 2025

    Stefan Hoffelner. On a local variant of the 12th Delfino problem, 2025. Preprint

    work page 2025

  20. [20]

    A universe with a∆1 n-definable well-order of the reals,CHandΠ 1 n- uniformization.arXiv preprint arXiv:2506.21778, 2025

    Stefan Hoffelner. A universe with a∆1 n-definable well-order of the reals,CHandΠ 1 n- uniformization.arXiv preprint arXiv:2506.21778, 2025

    work page arXiv 2025

  21. [21]

    A universe with large continuum, globalΣ-uniformization and a projective well-order of its reals.arXiv preprint arXiv:2506.12393, 2025

    Stefan Hoffelner. A universe with large continuum, globalΣ-uniformization and a projective well-order of its reals.arXiv preprint arXiv:2506.12393, 2025

    work page arXiv 2025

  22. [22]

    Stefan Hoffelner.MA(I)and a failure of separation on the third level.Annals of Pure and Applied Logic, 177(3):103667, 2026

    work page 2026

  23. [23]

    On $\boldsymbol{\Sigma}^1_3$- and $\Sigma^1_4$-uniformization

    Stefan Hoffelner. OnΣ 1 3- andΣ 1 4-uniformization.arXiv preprint arXiv:2604.19360, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  24. [24]

    Larson, Ralf Schindler, and Liuzhen Wu

    Stefan Hoffelner, Paul B. Larson, Ralf Schindler, and Liuzhen Wu. Forcing axioms and the definability of the nonstationary ideal on the first uncountable.Journal of Symbolic Logic, 89(4):1641–1658, 2024

    work page 2024

  25. [25]

    Borel∗ sets in the generalized Baire space and in- finitary languages

    Tapani Hyttinen and Vadim Kulikov. Borel∗ sets in the generalized Baire space and in- finitary languages. In Hans van Ditmarsch and Gabriel Sandu, editors,Jaakko Hintikka on Knowledge and Game-Theoretical Semantics, volume 12 ofOutstanding Contribu- tions to Logic, pages 395–412. Springer, Cham, 2018

    work page 2018

  26. [26]

    Springer Monographs in Mathematics

    Thomas Jech.Set Theory. Springer Monographs in Mathematics. Springer, third millennium edition, 2003

    work page 2003

  27. [27]

    Jensen and Robert M

    Ronald B. Jensen and Robert M. Solovay. Some applications of almost disjoint sets. InMathematical Logic and Foundations of Set Theory, volume 59 ofStudies in Logic and the Foundations of Mathematics, pages 84–104. North-Holland, 1970. 28

    work page 1970

  28. [28]

    Kechris.Classical Descriptive Set Theory, volume 156 ofGraduate Texts in Mathematics

    Alexander S. Kechris.Classical Descriptive Set Theory, volume 156 ofGraduate Texts in Mathematics. Springer, 1995

    work page 1995

  29. [29]

    Questions on generalised Baire spaces.Mathematical Logic Quarterly, 62(4–5):439–456, 2016

    Yurii Khomskii, Giorgio Laguzzi, Benedikt Löwe, and Ilya Sharankou. Questions on generalised Baire spaces.Mathematical Logic Quarterly, 62(4–5):439–456, 2016

    work page 2016

  30. [30]

    Philipp Lücke.Σ 1 1-definability at uncountable regular cardinals.Journal of Symbolic Logic, 77(3):1011–1046, 2012

    work page 2012

  31. [31]

    The Hurewicz dichotomy for generalized Baire spaces.Israel Journal of Mathematics, 216(2):973–1022, 2016

    Philipp Lücke, Luca Motto Ros, and Philipp Schlicht. The Hurewicz dichotomy for generalized Baire spaces.Israel Journal of Mathematics, 216(2):973–1022, 2016

    work page 2016

  32. [32]

    Continuous images of closed sets in generalized Baire spaces.Israel Journal of Mathematics, 209(1):421–461, 2015

    Philipp Lücke and Philipp Schlicht. Continuous images of closed sets in generalized Baire spaces.Israel Journal of Mathematics, 209(1):421–461, 2015

    work page 2015

  33. [33]

    Trees andΠ1 1-subsets of ω1ω1.Journal of Symbolic Logic, 58(3):1052–1070, 1993

    Alan Mekler and Jouko Väänänen. Trees andΠ1 1-subsets of ω1ω1.Journal of Symbolic Logic, 58(3):1052–1070, 1993

    work page 1993

  34. [34]

    Tadatoshi Miyamoto.ω1-Souslin trees under countable support iterations.Fundamenta Mathematicae, 142(3):257–261, 1993

    work page 1993

  35. [35]

    Moschovakis.Descriptive Set Theory, volume 155 ofMathematical Surveys and Monographs

    Yiannis N. Moschovakis.Descriptive Set Theory, volume 155 ofMathematical Surveys and Monographs. American Mathematical Society, 2009. 29

    work page 2009