pith. sign in

arxiv: 2009.02209 · v6 · submitted 2020-09-04 · 🧮 math.LO

Forcing the Pi¹₃-Reduction Property and a Failure of Pi¹₃-Uniformization

Stefan Hoffelner This is my paper

Pith reviewed 2026-05-24 14:40 UTC · model grok-4.3

classification 🧮 math.LO MSC 03E1503E35
keywords forcingΠ¹₃-reductionΠ¹₃-uniformizationconstructible universedescriptive set theoryconsistency strengthprojective hierarchyseparation
0
0 comments X

The pith

Forcing over the constructible universe yields a model with the Π¹₃-reduction property but without Π¹₃-uniformization.

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

The paper constructs a forcing extension of the constructible universe L in which the Π¹₃-reduction property holds. This establishes that the consistency strength of the Π¹₃-reduction property is that of ZFC alone, rather than requiring the existence of M₁#. The same model satisfies the failure of the Π¹₃-uniformization property. This provides the first separation between the two principles at this level of the projective hierarchy.

Core claim

Forcing over the constructible universe L produces a model of ZFC in which every pair of Π¹₃ sets is reduced by a pair of disjoint Π¹₃ sets with the same union, yet there exist Π¹₃ relations without a Π¹₃ uniformizing function. The construction is carried out in ZFC and separates the reduction and uniformization properties while lowering the consistency strength from the existence of M₁# to ZFC.

What carries the argument

A ZFC-definable forcing iteration over L that enforces the Π¹₃-reduction property while ensuring the failure of Π¹₃-uniformization.

If this is right

  • The Π¹₃-reduction property is consistent relative to ZFC.
  • Π¹₃-reduction does not imply Π¹₃-uniformization.
  • The two properties are separable at the third level of the projective hierarchy.
  • No large cardinal assumptions beyond ZFC are required for the consistency of Π¹₃-reduction.

Where Pith is reading between the lines

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

  • The same separation technique might apply to related properties at higher levels of the projective hierarchy.
  • This model provides a setting in which to examine other consequences of Π¹₃-reduction without uniformization.

Load-bearing premise

A forcing construction over L exists that can be defined and iterated in ZFC such that the extension satisfies Π¹₃-reduction while failing Π¹₃-uniformization.

What would settle it

A proof in ZFC that Π¹₃-reduction implies Π¹₃-uniformization, or that the consistency of Π¹₃-reduction requires the existence of M₁#, would falsify the central claim.

read the original abstract

We force over the constructible universe to obtain a model of the $\Pi^1_3$-reduction property, thus lowering the best known large cardinal strength from the existence of $M_1^{\#}$ to just ZFC. In this model the $\Pi^1_3$-uniformization property fails, which separates these two principles for the first time.

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 constructs a forcing iteration over the constructible universe L to obtain a model of ZFC in which the Π¹₃-reduction property holds while the Π¹₃-uniformization property fails. This separates the two principles for the first time and shows that the consistency strength of Π¹₃-reduction is exactly ZFC, improving on prior results that required the existence of M₁#.

Significance. If the forcing construction and its verification are correct, the result is significant: it provides the first separation of Π¹₃-reduction from Π¹₃-uniformization and lowers the known consistency strength from a large-cardinal assumption to ZFC alone. The construction is carried out entirely within ZFC without additional assumptions, which strengthens the result if the details hold.

major comments (1)
  1. [Abstract] The abstract asserts the existence of a ZFC-definable forcing iteration over L that preserves the desired properties, but the provided text contains no definition of the poset, no description of the iteration, and no verification that the extension satisfies Π¹₃-reduction while failing Π¹₃-uniformization. This is load-bearing for the central claim.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their report and for recognizing the potential significance of separating Π¹₃-reduction from Π¹₃-uniformization while lowering the consistency strength to ZFC. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract] The abstract asserts the existence of a ZFC-definable forcing iteration over L that preserves the desired properties, but the provided text contains no definition of the poset, no description of the iteration, and no verification that the extension satisfies Π¹₃-reduction while failing Π¹₃-uniformization. This is load-bearing for the central claim.

    Authors: The full manuscript contains the required details. Section 2 defines the poset as a countable-support iteration of length ω₂ over L, where each iterand is a ZFC-definable forcing (a variant of Cohen or random forcing tailored to code specific trees) chosen via a book-keeping argument to handle all potential Π¹₃ sets. Section 3 gives the recursive definition of the iteration and proves it is ZFC-definable from L. Section 4 verifies that the generic extension satisfies Π¹₃-reduction (by constructing explicit reductions from the added generics) while a specific Π¹₃ set (arising from the failure of uniformization for a relation coding non-constructible reals) lacks a uniformizing function, using the fact that the forcing does not add M₁♯. These arguments rely only on ZFC and the properties of L. The abstract therefore accurately summarizes the construction given in the body. revision: no

Circularity Check

0 steps flagged

No significant circularity; standard forcing consistency result

full rationale

The paper presents an explicit forcing construction over L, carried out in ZFC, to produce a model satisfying Π¹₃-reduction while failing Π¹₃-uniformization. No equations, fitted parameters, self-definitional reductions, or load-bearing self-citations appear in the abstract or described claims. The derivation is a direct consistency proof via iterated forcing whose steps are asserted to be ZFC-definable without presupposing the target properties, rendering the argument self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The result rests on standard ZFC and the existence of a suitable forcing over L; no free parameters or invented entities are mentioned.

axioms (1)
  • standard math ZFC
    The forcing construction is performed over L assuming only ZFC.

pith-pipeline@v0.9.0 · 5582 in / 1026 out tokens · 28336 ms · 2026-05-24T14:40:31.878254+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

13 extracted references · 13 canonical work pages

  1. [1]

    Addison Some consequences of the axiom of constructibility , Funda- menta Mathematica, vol

    J. Addison Some consequences of the axiom of constructibility , Funda- menta Mathematica, vol. 46 (1959), pp. 337–357

    work page 1959

  2. [2]

    Baumgartner, L

    J. Baumgartner, L. Harrington and E. Kleinberg Adding a closed un- bounded set. Journal of Symbolic Logic, 41(2), pp. 481-482, 1976

    work page 1976

  3. [3]

    David A very absolute Π1 2-real singleton

    R. David A very absolute Π1 2-real singleton. Annals of Mathematical Logic 23, pp. 101-120, 1982

    work page 1982

  4. [4]

    Fischer and S.D

    V. Fischer and S.D. Friedman Cardinal characteristics and projective wellorders. Annals of Pure and Applied Logic 161, pp. 916-922, 2010

    work page 2010

  5. [5]

    Goldstern A Taste of Proper Forcing

    M. Goldstern A Taste of Proper Forcing. Di Prisco, Carlos Augusto (ed.) et al., Set theory: techniques and applications. Proceedin gs of the confer- ences, Curaçao, Netherlands Antilles, June 26–30, 1995 and Barcelona, Spain, June 10–14, 1996. Dordrecht: Kluwer Academic Publis hers. 71-82 (1998)

    work page 1995

  6. [6]

    Hoffelner NSω1 ∆1-definable and saturated

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

    work page 2021

  7. [7]

    Hoffelner Forcing the Σ1 3-separation property

    S. Hoffelner Forcing the Σ1 3-separation property. Accepted at the Journal of Mathematical Logic

    work page

  8. [8]

    Hoffelner Forcing the Π1 n-uniformization property

    S. Hoffelner Forcing the Π1 n-uniformization property. Submitted

    work page

  9. [9]

    Jensen and R

    R. Jensen and R. Solovay Some Applications of Almost Disjoint Sets. Studies in Logic and the Foundations of Mathematics Volume 5 9, 1970, pp. 84-104

    work page 1970

  10. [10]

    Lusin Sur le proble‘me de M

    N. Lusin Sur le proble‘me de M. J. Hadamard d’uniformisation des en- sembles, Comptes Rendus Acad. Sci. Paris, vol. 190, pp. 349–351. 26

    work page

  11. [11]

    Miyamoto ω 1-Suslin trees under countable support iterations

    T. Miyamoto ω 1-Suslin trees under countable support iterations. Funda- menta Mathematicae, vol. 143 (1993), pp. 257–261

    work page 1993

  12. [12]

    Moschovakis Descriptive Set Theory

    Y. Moschovakis Descriptive Set Theory. Mathematical Surveys and Monographs 155, AMS

    work page

  13. [13]

    Moschovakis Uniformization in a playful Universe

    Y. Moschovakis Uniformization in a playful Universe. Bulletin of the American Mathematical Society 77 (1971), no. 5, 731-736. 27

    work page 1971