pith. sign in

arxiv: 2606.25590 · v2 · pith:WHVCAAVHnew · submitted 2026-06-24 · 🧮 math.LO · cs.LO

Bar-recursion and Preservation of Cardinals

Laura Fontanella , Jacopo Furlan This is my paper

Pith reviewed 2026-06-30 10:11 UTC · model grok-4.3

classification 🧮 math.LO cs.LO
keywords bar-recursionrealizability algebrascardinal preservationaxiom of choiceclassical realizabilitytransfinite recursionset theory
0
0 comments X

The pith

Generalized bar-recursion in κ-fully-closed realizability algebras makes every cardinal up to κ remain a cardinal in the model.

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

The paper introduces a transfinite form of bar-recursion inside classical realizability models for set theory. This extension constructs models that satisfy uncountable fragments of the axiom of choice. The work defines an analogue of κ-closure called κ-full-closure for realizability algebras and proves that, under this property, the generalized recursion realizes the preservation of all cardinals ≤ κ. A sympathetic reader cares because the result links a computational principle directly to cardinal arithmetic inside realizability interpretations.

Core claim

In realizability algebras satisfying the κ-full-closure property, generalized bar-recursion realizes that any cardinal up to κ admits a representative in the realizability model which remains a cardinal.

What carries the argument

The κ-full-closure property on classical realizability algebras, which serves as the condition enabling transfinite bar-recursion to preserve cardinals.

If this is right

  • Uncountable fragments of the axiom of choice become realizable in the constructed models.
  • Previous countable-choice results from bar-recursion extend to larger cardinals.
  • Cardinal preservation becomes a direct consequence of the algebraic closure condition rather than an extra assumption.

Where Pith is reading between the lines

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

  • The same closure condition might be checked directly on known realizability algebras to obtain new preservation results without rebuilding the model.
  • The technique could be tested on specific large cardinals by varying κ and examining the resulting choice principles.
  • It opens a route to compare how realizability and forcing handle the same closure properties for cardinal arithmetic.

Load-bearing premise

The transfinite bar-recursion and the κ-full-closure property can be defined and realized inside the target algebras without introducing inconsistencies.

What would settle it

An explicit realizability algebra that meets the κ-full-closure property yet whose model contains a collapsed cardinal ≤ κ.

read the original abstract

This work presents a transfinite version of the bar-recursion in the context of classical realizability models for set theory. Bar-recursion has been previously used to obtain realizability interpretations of countable choice and dependent choice, and was employed by Krivine to realize the continuum hypothesis in classical realizability. In this paper, we introduce a transfinite variant of bar-recursion and use it to construct realizability models validating uncountable fragments of the Axiom of Choice. Moreover, our construction reveals that this generalized bar-recursion is related to preservation of cardinals. To show this, we define an analogue of the forcing notion of $\kappa$-closure for classical realizability algebras that we call $\kappa$-fully-closed. We show that, in realizability algebras satisfying the $\kappa$-full-closure property, generalized bar-recursion realizes that any cardinal up to $\kappa$ admits a representative in the realizability model which remains a cardinal.

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 / 3 minor

Summary. The paper introduces a transfinite generalization of bar-recursion in classical realizability algebras for set theory. Building on prior uses of bar-recursion for countable choice and the continuum hypothesis, it defines an analogue of κ-closure called the κ-full-closure property for realizability algebras. The central claim is that, in algebras satisfying this property, the generalized bar-recursion realizes that every cardinal ≤ κ has a representative in the realizability model that remains a cardinal.

Significance. If the constructions are correct, the result extends realizability interpretations to uncountable choice fragments while linking bar-recursion directly to cardinal preservation, providing a new tool for controlling the set-theoretic content of realizability models. The explicit analogy to forcing notions of closure is a useful conceptual bridge.

minor comments (3)
  1. The abstract states that the generalized bar-recursion 'realizes that any cardinal up to κ admits a representative... which remains a cardinal,' but the manuscript should include an explicit statement of the precise formula or principle being realized (e.g., the relevant instance of 'κ is a cardinal' in the model language) to make the preservation claim fully precise.
  2. The definition of the κ-full-closure property for realizability algebras is introduced as an analogue of forcing closure; the paper would benefit from a short comparison paragraph noting which forcing properties are preserved or lost under the realizability translation.
  3. The manuscript should clarify whether the transfinite bar-recursion is defined by recursion on ordinals inside the algebra or externally, and whether this requires any additional consistency strength beyond the background theory of the algebra.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the paper and the recommendation of minor revision. The work defines a transfinite generalization of bar-recursion together with the κ-full-closure property for realizability algebras, showing that this realizes uncountable choice fragments while preserving cardinals ≤ κ. No specific major comments appear in the report, so we have no individual points requiring rebuttal or revision at this stage.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The provided abstract and description introduce new definitions (transfinite bar-recursion and the κ-full-closure property) and derive consequences for cardinal preservation in realizability algebras. No load-bearing steps reduce claims to self-definitions, fitted parameters renamed as predictions, or self-citation chains. The central result is framed as a consequence of the new constructions rather than equivalent to inputs by construction. This is the expected non-finding for a paper presenting novel definitions and their independent consequences.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The claims rest on the new definitions of transfinite bar-recursion and κ-full-closure together with background assumptions of classical realizability; no free parameters are mentioned.

axioms (1)
  • domain assumption Standard background results of classical realizability and set theory
    The constructions are carried out inside existing realizability models for set theory.
invented entities (2)
  • transfinite bar-recursion no independent evidence
    purpose: realize uncountable fragments of the axiom of choice
    New variant introduced to extend prior countable bar-recursion
  • κ-fully-closed realizability algebra no independent evidence
    purpose: ensure cardinals up to κ remain cardinals in the model
    New analogue of κ-closure defined for this realizability setting

pith-pipeline@v0.9.1-grok · 5686 in / 1193 out tokens · 42496 ms · 2026-06-30T10:11:28.882780+00:00 · methodology

Review history (2 revisions) →

discussion (0)

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

Reference graph

Works this paper leans on

30 extracted references · 2 canonical work pages

  1. [1]

    IEEE, 2021

    BeniaminoAccattoli, UgoDalLago, andGabrieleVanoni.Thespaceofinteraction.In36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13. IEEE, 2021

    2021

  2. [2]

    North-Holland, 1985

    Hendrik Pieter Barendregt.The lambda calculus - its syntax and semantics, volume 103 ofStudies in logic and the foundations of mathematics. North-Holland, 1985

    1985

  3. [3]

    Bell.Set Theory: Boolean-Valued Models and Independence Proofs

    John L. Bell.Set Theory: Boolean-Valued Models and Independence Proofs. Oxford Logic Guides. Oxford University Press, 2005

    2005

  4. [4]

    On the computational content of the axiom of choice

    Stefano Berardi, Marc Bezem, and Thierry Coquand. On the computational content of the axiom of choice. J. Symb. Log., 63(2):600–622, 1998

    1998

  5. [5]

    Lecture Notes in Logic

    Ulrich Berger and Paulo Oliva.Modified bar recursion and classical dependent choice, page 89–107. Lecture Notes in Logic. Cambridge University Press, 2005. 28 LAURA FONTANELLA AND JACOPO FURLAN

    2005

  6. [6]

    Constructive characterisations of the must-preorder for asynchrony

    Giovanni Bernardi, Ilaria Castellani, Paul Laforgue, and Léo Stefanesco. Constructive characterisations of the must-preorder for asynchrony. In Viktor Vafeiadis, editor,Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, H...

    2025

  7. [7]

    On bar recursion and choice in a classical setting

    Valentin Blot and Colin Riba. On bar recursion and choice in a classical setting. In Chung-chieh Shan, editor, Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings, Lecture Notes in Computer Science, pages 349–364. Springer, 2013

    2013

  8. [8]

    On the logical structure of choice and bar induction principles

    Nuria Brede and Hugo Herbelin. On the logical structure of choice and bar induction principles. In36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13. IEEE, 2021

    2021

  9. [9]

    L. E. J. Brouwer. Über definitionsbereiche von funktionen.Mathematische Annalen, 97(1):60–75, 1927. Intro- duces the bar theorem, foundational to bar induction in intuitionistic analysis

    1927

  10. [10]

    Realizability in the Unitary Sphere

    Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, and Benoît Valiron. Realizability in the Unitary Sphere. In34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), Vancouver, Canada, June 2019

    2019

  11. [11]

    Böhm trees, krivine’s machine and the taylor expansion of lambda- terms

    Thomas Ehrhard and Laurent Regnier. Böhm trees, krivine’s machine and the taylor expansion of lambda- terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors,Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006, Proceedings, volume 3988 ofLectur...

    2006

  12. [12]

    Friedman, Eugene E

    Matthias Felleisen, Daniel P. Friedman, Eugene E. Kohlbecker, and Bruce F. Duba. Reasoning with continua- tions. InProceedings of the Symposium on Logic in Computer Science (LICS ’86), Cambridge, Massachusetts, USA, June 16-18, 1986, pages 131–141. IEEE Computer Society, 1986

    1986

  13. [13]

    Preserving cardinals and weak forms of zorn’s lemma in realizability models.Math

    Laura Fontanella and Guillaume Geoffroy. Preserving cardinals and weak forms of zorn’s lemma in realizability models.Math. Struct. Comput. Sci., 30(9):976–996, 2020

    2020

  14. [14]

    Realizing the totally unordered structure of ordinals.CoRR, abs/2504.03532, 2025

    Laura Fontanella and Richard Matthews. Realizing the totally unordered structure of ordinals.CoRR, abs/2504.03532, 2025

    work page arXiv 2025

  15. [15]

    The consistency of classical set theory relative to a set theory with intuitionistic logic.J

    Harvey Friedman. The consistency of classical set theory relative to a set theory with intuitionistic logic.J. Symb. Log., 38(2):315–319, 1973

    1973

  16. [16]

    A formulae-as-types notion of control

    Timothy Griffin. A formulae-as-types notion of control. In Frances E. Allen, editor,Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, pages 47–58. ACM Press, 1990

    1990

  17. [17]

    The ordering principle and higher dependent choice, 2025

    Peter Holy and Jonathan Schilhan. The ordering principle and higher dependent choice, 2025

    2025

  18. [18]

    On the interpretation of intuitionistic number theory.J

    Stephen Cole Kleene. On the interpretation of intuitionistic number theory.J. Symb. Log., 10(4):109–124, 1945

    1945

  19. [19]

    Typed lambda-calculus in classical zermelo-frænkel set theory.Arch

    Jean-Louis Krivine. Typed lambda-calculus in classical zermelo-frænkel set theory.Arch. Math. Log., 40(3):189–205, 2001

    2001

  20. [20]

    Realizability algebras II : new models of ZF + DC.Log

    Jean-Louis Krivine. Realizability algebras II : new models of ZF + DC.Log. Methods Comput. Sci., 8(1), 2012

    2012

  21. [21]

    On the structure of classical realizability models of ZF

    Jean-Louis Krivine. On the structure of classical realizability models of ZF. In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors,20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France, volume 39 ofLIPIcs, pages 146–161. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014

    2014

  22. [22]

    Bar recursion in classical realisability: Dependent choice and continuum hypothesis

    Jean-Louis Krivine. Bar recursion in classical realisability: Dependent choice and continuum hypothesis. In Jean-Marc Talbot and Laurent Regnier, editors,25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 ofLIPIcs, pages 25:1–25:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016

    2016

  23. [23]

    Realizability algebras III: some examples.Math

    Jean-Louis Krivine. Realizability algebras III: some examples.Math. Struct. Comput. Sci., 28(1):45–76, 2018

    2018

  24. [24]

    A program for the full axiom of choice.Log

    Jean-Louis Krivine. A program for the full axiom of choice.Log. Methods Comput. Sci., 17(3), 2021

    2021

  25. [25]

    Springer Berlin Heidelberg, 1973

    Horst Luckhardt.Extensional Gödel Functional Interpretation. Springer Berlin Heidelberg, 1973

    1973

  26. [26]

    A guide to krivine realizability for set theory.CoRR, abs/2307.13563, 2023

    Richard Matthews. A guide to krivine realizability for set theory.CoRR, abs/2307.13563, 2023

    work page arXiv 2023

  27. [27]

    Implicative algebras: a new foundation for realizability and forcing.Math

    Alexandre Miquel. Implicative algebras: a new foundation for realizability and forcing.Math. Struct. Comput. Sci., 30(5):458–510, 2020. BAR-RECURSION AND PRESER V ATION OF CARDINALS 29

    2020

  28. [28]

    Constable

    Vincent Rahli, Mark Bickford, Liron Cohen, and Robert L. Constable. Bar induction is compatible with constructive type theory.J. ACM, 66(2):13:1–13:35, 2019

    2019

  29. [29]

    Provably recursive functionals of analysis: a consistency proof of analysis by an extension of princ

    Clifford Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of princ. 1962

    1962

  30. [30]

    A classical realizability model arising from a stable model of untyped lambda calculus.Log

    Thomas Streicher. A classical realizability model arising from a stable model of untyped lambda calculus.Log. Methods Comput. Sci., 13(4), 2017. Univ Paris Est Creteil, LACL, [F-94010 Creteil, France] Email address:laura.fontanella@u-pec.fr Laboratoire d’Informatique de Paris Nord, Université Sorbonne Paris Nord, and Univ Paris Est Creteil, LACL, [F-94010...

    2017