pith. sign in

arxiv: 2606.08176 · v1 · pith:XBKNGA2Tnew · submitted 2026-06-06 · 🧮 math.LO

Constructive Stone representations for separated swap and Boolean algebras

Daniel Misselbeck-Wessel , Iosif Petrakis This is my paper

Pith reviewed 2026-06-27 18:56 UTC · model grok-4.3

classification 🧮 math.LO
keywords swap algebrasStone representationBoolean algebrasconstructive mathematicsseparated algebrasStone-Cech theoremBoolean inequalityminimal logic
0
0 comments X

The pith

Separated swap algebras of type (II) admit a constructive Stone representation.

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

The paper establishes a constructive Stone representation theorem for separated swap algebras of type (II). Swap algebras generalize Bishop's complemented powerset in the same manner that Boolean algebras generalize the powerset, and every Boolean algebra is already a swap algebra. The authors introduce sets carrying a Boolean inequality to track the ex falso principle, which lets the representation proof remain inside minimal logic when this extra structure is present. They further prove a Stone-Cech theorem for swap algebras of type (II), which shows that restricting attention to the separated case loses no generality for the theory of swap characters. Both results specialize directly to yield constructive Stone theorems for Boolean algebras.

Core claim

We prove constructively a Stone representation theorem for separated swap algebras of type (II), where the notion of a separated swap algebra generalises the corresponding notion of a separated Boolean algebra. Moreover, we prove a Stone-Cech theorem for swap algebras of type (II), showing that the restriction to separated swap algebras is not a loss of generality from the point of view of the theory of swap characters. A constructive Stone representation theorem and a Stone-Cech theorem for Boolean algebras follow as special cases. We introduce sets with a Boolean inequality, that is sets with an internal falsum. If we restrict to swap algebras with a Boolean inequality, then the proof of t

What carries the argument

The separated swap algebra of type (II) together with the optional Boolean inequality that controls ex falso usage.

If this is right

  • Every separated Boolean algebra admits a constructive Stone representation as a special case.
  • The full theory of swap characters for type-(II) algebras is captured by the separated subclass via the Stone-Cech theorem.
  • When a Boolean inequality is added, the entire representation argument stays inside minimal logic.
  • The same bookkeeping device extends the reach of constructive representation theorems to structures that generalize complemented powersets.

Where Pith is reading between the lines

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

  • The Boolean-inequality device may transfer to other algebraic representation theorems that currently rely on classical ex-falso steps.
  • Pointfree or locale-theoretic constructions in Bishop mathematics could be simplified by working directly with swap algebras rather than Boolean algebras alone.
  • The separation condition may turn out to be the minimal extra datum needed to make many other classical representation results constructive.

Load-bearing premise

The separation condition together with the type-(II) classification suffices for the representation without invoking classical principles beyond those tracked by the Boolean inequality.

What would settle it

An explicit construction, inside minimal logic, of a separated swap algebra of type (II) whose swap characters do not separate points in the required way.

read the original abstract

Swap algebras generalise Bishop's complemented powerset as Boolean algebras generalise the powerset. Actually, all Boolean algebras are swap algebras. We prove constructively a Stone representation theorem for separated swap algebras of type (II), where the notion of a separated swap algebra generalises the corresponding notion of a separated Boolean algebra. Moreover, we prove a Stone-Cech theorem for swap algebras of type (II), showing that the restriction to separated swap algebras is not a loss of generality from the point of view of the theory of swap characters. A constructive Stone representation theorem and a Stone-Cech theorem for Boolean algebras follow as special cases. We introduce sets with a Boolean inequality, that is sets with an internal falsum. These sets allow a book-keeping of the use of the Ex falso principle in constructive mathematics. If we restrict to swap algebras with a Boolean inequality, then the proof of the Stone representation theorem for swap algebras of type (II) is within minimal logic.

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

Summary. The manuscript introduces swap algebras, which generalize Boolean algebras (and in particular Bishop's complemented powerset), and proves constructively a Stone representation theorem for separated swap algebras of type (II). It further establishes a Stone-Čech theorem for swap algebras of type (II), showing that the separation restriction is not a loss of generality for the theory of swap characters. Boolean algebras arise as a special case. The paper introduces sets equipped with a Boolean inequality (an internal falsum) to track and restrict applications of ex falso, allowing the representation proof to remain within minimal logic when this structure is present.

Significance. If the stated proofs hold, the work supplies a constructive representation theorem in a setting that properly generalizes Boolean algebras while controlling the logical strength via the Boolean-inequality device. This is a useful bookkeeping tool for constructive algebra and recovers the corresponding Boolean results as special cases. The type-(II) classification and separation condition are presented as sufficient to carry the representation without additional classical principles.

minor comments (2)
  1. [Abstract] Abstract: the phrase 'separated swap algebra of type (II)' is introduced without a one-sentence gloss; a parenthetical reminder of the two key properties would aid readers who encounter the main theorem statement first.
  2. [Introduction] The manuscript would benefit from an explicit statement, early in the introduction, of how the Boolean-inequality structure interacts with the separation axiom in the proof of the representation map (currently described only at the level of the abstract).

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading and positive evaluation of the manuscript. The recommendation for minor revision is noted, but no specific major comments were raised in the report.

Circularity Check

0 steps flagged

Derivation is self-contained; no circular reductions identified

full rationale

The paper establishes a constructive Stone representation theorem for separated swap algebras of type (II) via explicit definitions and proofs that track the Boolean inequality to restrict ex falso. The separation condition and type-(II) classification are used to construct the representation map directly, with Boolean algebras recovered as a special case. No step reduces a claimed prediction or theorem to a fitted parameter, self-citation chain, or definitional renaming; the argument remains within minimal logic when the inequality is present and is independent of external fitted data or prior author-specific uniqueness results.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

Abstract-only review; swap algebras and separated type-(II) variants are introduced as new structures. Standard constructive mathematics background is assumed.

axioms (2)
  • domain assumption Bishop-style constructive mathematics
    The entire development is carried out constructively, as stated in the abstract.
  • domain assumption Minimal logic suffices when Boolean inequality is present
    Claimed explicitly for the restricted case in the abstract.
invented entities (2)
  • swap algebra no independent evidence
    purpose: Generalization of Boolean algebra that extends complemented powersets
    Introduced in the abstract as the central new object.
  • separated swap algebra of type (II) no independent evidence
    purpose: The subclass for which the Stone representation holds
    Defined in the abstract as the setting of the main theorem.

pith-pipeline@v0.9.1-grok · 5694 in / 1272 out tokens · 29279 ms · 2026-06-27T18:56:23.002788+00:00 · methodology

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

54 extracted references · 7 canonical work pages

  1. [1]

    Aczel, M

    P. Aczel, M. Rathjen:Notes on Constructive Set Theory, Report No. 40, 2000/2001, ISSN 1103- 467X. Institut Mittag-Leffler

    2000

  2. [2]

    B. D. Arendt, C. J. Stuth: On partial homomorphisms of semigroups, Pacific Journal of Mathe- matics, Vol. 35, No. 1, 1970, 7–9

    1970

  3. [3]

    Bezhanishvili, W

    N. Bezhanishvili, W. H. Holliday: Choice-Free Stone Duality, The Journal of Symbolic Logic, Vol. 85, No. 1, 2020, pp. 109–148

    2020

  4. [4]

    Bishop: The Constructivization of Abstract Mathematical Analysis, Proc

    E. Bishop: The Constructivization of Abstract Mathematical Analysis, Proc. Int’l. Congr.Math., Moscow, 1966, 308-313

    1966

  5. [5]

    Bishop:Foundations of Constructive Analysis, McGraw-Hill, 1967

    E. Bishop:Foundations of Constructive Analysis, McGraw-Hill, 1967

    1967

  6. [6]

    Bishop, H

    E. Bishop, H. Cheng:Constructive Measure Theory, Mem. Amer. Math. Soc. 116, 1972

    1972

  7. [7]

    Bishop, D

    E. Bishop, D. S. Bridges:Constructive Analysis, Grundlehren der math. Wissenschaften 279, Springer-Verlag, Heidelberg-Berlin-New York, 1985. 25

    1985

  8. [8]

    Blechschmidt, P

    I. Blechschmidt, P. Schuster: Reifying dynamical algebra: Maximal ideals in countable rings, constructively, Computability, 13, 2024, 263–297

    2024

  9. [9]

    F. F. Bonsal, J. Duncan,Complete Normed Algebras, Springer-Verlag, 1973

    1973

  10. [10]

    D. S. Bridges:Constructive Functional Analysis, Research Notes in Mathematics No. 28. Pitman Advanced Publishing Programme, London, 1979

    1979

  11. [11]

    D. S. Bridges, F. Richman:Varieties of Constructive Mathematics, Cambridge University Press, 1987

    1987

  12. [12]

    D. S. Bridges and L. S. Vîţă:Techniques of Constructive Analysis, in: Universitext, Springer, New York, 2006

    2006

  13. [13]

    Y. K. Chan:Foundations of Constructive Probability Theory, volume 177, Cambridge University Press, 2021

    2021

  14. [14]

    Ciraulo and G

    F. Ciraulo and G. Sambin: Finitary formal topologies and Stone’s representation theorem, Theo- retical Computer Science 405, 2008, 11–23

    2008

  15. [15]

    Coquand, E

    T. Coquand, E. Palmgren: Metric Boolean algebras and constructive measure theory, Arch. Math. Logic 41, 2002, 687–704

    2002

  16. [16]

    T.Coquand, B.Spitters: ConstructiveGelfanddualityforC ˚-algebras, MathematicalProceedings of the Cambridge Philosophical Society, Volume 147, Issue 02, 2009, pp. 339–344

    2009

  17. [17]

    Diener: Constructive Reverse Mathematics, arXiv:1804.05495, 2020

    H. Diener: Constructive Reverse Mathematics, arXiv:1804.05495, 2020

    work page arXiv 2020

  18. [18]

    R. S. Doran, V. Belfi: Characterizations ofC˚-Algebras, Marcel Dekker, Inc., 1986

    1986

  19. [19]

    Feferman: Constructive Theories of Functions and Classes, in Boffa et

    S. Feferman: Constructive Theories of Functions and Classes, in Boffa et. al (Eds.)Logic Collo- quium ’78, Elsevier, 1979, 159–224

    1979

  20. [20]

    Gillman, M

    L. Gillman, M. Jerison:Rings of Continuous Functions, Van Nostrand, 1960

    1960

  21. [21]

    F. L. Grubmüller, I. Petrakis: A Predicative Approach to the Constructive Integration Theory of Locally Compact Metric Spaces, Journal of Logic and Analysis, Vol. 17, 2025, 1–24

    2025

  22. [22]

    P. R. Halmos:Lectures on Boolean Algebras, Springer-Verlag, 1974

    1974

  23. [23]

    Herrlich:Topologische Reflexionen und Coreflexionen, Lecture Notes in Mathematics, Springer, 1968

    H. Herrlich:Topologische Reflexionen und Coreflexionen, Lecture Notes in Mathematics, Springer, 1968

    1968

  24. [24]

    N. Köpp, I. Petrakis: Strong negation in the theory of computable functionals TCF, arXiv:2210.05491v3, 2023

    work page arXiv 2023

  25. [25]

    Lombardi, C

    H. Lombardi, C. Quitté:Commutative Algebra: Constructive Methods, Springer, 2015

    2015

  26. [26]

    Martin-Löf: An intuitionistic theory of types: predicative part, in H

    P. Martin-Löf: An intuitionistic theory of types: predicative part, in H. E. Rose and J. C. Shep- herdson (Eds.)Logic Colloquium’73, Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pp.73-118, North-Holland, 1975

    1975

  27. [27]

    Martin-Löf: An intuitionistic theory of types, in G

    P. Martin-Löf: An intuitionistic theory of types, in G. Sambin, J. M. Smith (Eds.)Twenty- five years of constructive type theory(Venice, 1995), volume 36 of Oxford Logic Guides, Oxford University Press, 1998, 127–172

    1995

  28. [28]

    Misselbeck-Wessel, I

    D. Misselbeck-Wessel, I. Petrakis: Complemented subsets and Boolean-valued, partial functions, Computability, vol. 13, no. 3-4, 2024, pp. 399–431

    2024

  29. [29]

    Misselbeck-Wessel, I

    D. Misselbeck-Wessel, I. Petrakis: Boolean Rigs, Algebra Universalis 86, 29, 2025 https://doi.org/10.1007/s00012-025-00904-9 26

    work page doi:10.1007/s00012-025-00904-9 2025

  30. [30]

    Myhill: Constructive Set Theory, J

    J. Myhill: Constructive Set Theory, J. Symbolic Logic 40, 1975, 347–382

    1975

  31. [31]

    Mines, F

    R. Mines, F. Richman, W. Ruitenburg:A course in constructive algebra, Springer Science`Business Media New York, 1988

    1988

  32. [32]

    Negri: Stone bases, alias the constructive content of Stone representation, in A

    S. Negri: Stone bases, alias the constructive content of Stone representation, in A. Ursini, P. Aglianò (Eds.)Logic and Algebra, Dekker, New York, 1996, pp. 617–636

    1996

  33. [33]

    Palmgren: Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic 163, 2012, 1384–1399

    E. Palmgren: Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic 163, 2012, 1384–1399

    2012

  34. [34]

    Palmgren: Bishop-style constructive mathematics in type theory - A tutorial, Slides, 2013

    E. Palmgren: Bishop-style constructive mathematics in type theory - A tutorial, Slides, 2013. http://staff.math.su.se/palmgren/

    2013

  35. [35]

    Palmgren, O

    E. Palmgren, O. Wilander: Constructing categories and setoids of setoids in type theory, Logical Methods in Computer Science. 10 (2014), Issue 3, paper 25

    2014

  36. [36]

    Palmgren: Constructions of categories of setoids from proof-irrelevant families, Archive for Mathematical Logic 56, 2017, 51–66

    E. Palmgren: Constructions of categories of setoids from proof-irrelevant families, Archive for Mathematical Logic 56, 2017, 51–66

    2017

  37. [37]

    Palmgren: From type theory to setoids and back, preprint, 2019

    E. Palmgren: From type theory to setoids and back, preprint, 2019

    2019

  38. [38]

    Petrakis: Completely Regular Bishop Spaces, in A

    I. Petrakis: Completely Regular Bishop Spaces, in A. Beckmann, V. Mitrana and M. Soskova (Eds.):Evolving Computability, CiE 2015, LNCS 9136, 2015, 302–312

    2015

  39. [39]

    Petrakis: Dependent sums and Dependent Products in Bishop’s Set Theory, in P

    I. Petrakis: Dependent sums and Dependent Products in Bishop’s Set Theory, in P. Dybjer et. al. (Eds) TYPES 2018, LIPIcs, Vol. 130, Article No. 3, 2019

    2018

  40. [40]

    Petrakis:Families of Sets in Bishop Set Theory, Habilitationsschrift, LMU, Munich, 2020, available athttps://www.mathematik.uni-muenchen.de/„petrakis/

    I. Petrakis:Families of Sets in Bishop Set Theory, Habilitationsschrift, LMU, Munich, 2020, available athttps://www.mathematik.uni-muenchen.de/„petrakis/

    2020

  41. [41]

    Petrakis: Proof-relevance in Bishop-style constructive mathematics, Mathematical Structures in Computer Science, Volume 32, Issue 1, 2022, 1–43

    I. Petrakis: Proof-relevance in Bishop-style constructive mathematics, Mathematical Structures in Computer Science, Volume 32, Issue 1, 2022, 1–43. doi:10.1017/S0960129522000159

    work page doi:10.1017/s0960129522000159 2022

  42. [42]

    Constructive Mathematics: Foundation and Practice

    I. Petrakis: Topologies of open complemented subsets, in “Constructive Mathematics: Foundation and Practice”, M. Mitrović, M. N. Hounkonnou (Eds.), “Mathematics in Mind" series, Springer, 2025, forthcoming. Also available at arXiv:2312.17095v2, 2025

    work page arXiv 2025

  43. [43]

    Petrakis: Sets Completely Separated by Functions in Bishop Set Theory, Notre Dame Journal of Formal Logic, 65(2): 151-180 (May 2024) DOI: 10.1215/00294527-2024-0010

    I. Petrakis: Sets Completely Separated by Functions in Bishop Set Theory, Notre Dame Journal of Formal Logic, 65(2): 151-180 (May 2024) DOI: 10.1215/00294527-2024-0010

    work page doi:10.1215/00294527-2024-0010 2024

  44. [44]

    Petrakis: Strong negation in constructive mathematics, in preparation, 2026

    I. Petrakis: Strong negation in constructive mathematics, in preparation, 2026

    2026

  45. [45]

    Petrakis: Sets with a Boolean inequality, in preparation, 2026

    I. Petrakis: Sets with a Boolean inequality, in preparation, 2026

    2026

  46. [46]

    Petrakis, D

    I. Petrakis, D. Wessel: Algebras of complemented subsets, in U. Berger et.al. (Eds):Revolutions and Revelations in Computability, CiE 2022, Lecture Notes in Computer Science 13359, Springer, 2022, 246–258

    2022

  47. [47]

    2:1-2:33

    I.Petrakis, M.Zeuner: Pre-measurespacesandpre-integrationspacesinpredicativeBishop-Cheng measure theory, Logical Methods in Computer Science, Volume 20, Issue 4, 2024, pp. 2:1-2:33

    2024

  48. [48]

    Petrich: On extensions of semigroups determined by partial homomorphisms, Nederl

    M. Petrich: On extensions of semigroups determined by partial homomorphisms, Nederl. Akad. Wetensch. Indag. 28, 1966, 49–51

    1966

  49. [49]

    Rijke:Introduction to Homotopy Type Theory, https://arxiv.org/abs/2212.11082, 2022, pre- publication version, which will be published by Cambridge University Press

    E. Rijke:Introduction to Homotopy Type Theory, https://arxiv.org/abs/2212.11082, 2022, pre- publication version, which will be published by Cambridge University Press

    work page arXiv 2022

  50. [50]

    Richman: Algebraic Functions, Calculus Style, Communications in Algebra, 40, 2012, 2671– 2683

    F. Richman: Algebraic Functions, Calculus Style, Communications in Algebra, 40, 2012, 2671– 2683. 27

    2012

  51. [51]

    Stoltenberg-Hansen, J

    V. Stoltenberg-Hansen, J. V. Tucker: Computable and continuous partial homomorphisms on metric partial algebras, The Bulletin of Symbolic Logic, Volume 9, Number 3, 2003, 299–334

    2003

  52. [52]

    Takamura: An Introduction to the Theory ofC˚-Algebras in Constructive Mathematics, in P

    H. Takamura: An Introduction to the Theory ofC˚-Algebras in Constructive Mathematics, in P. Schuster, L. Crosilla (Eds.)From Sets and Types to Topology and Analysis, Oxford University Press, 2005, pp. 280–292

    2005

  53. [53]

    The Univalent Foundations Program:Homotopy Type Theory: Univalent Foundations of Mathe- matics, Institute for Advanced Study, Princeton, 2013

    2013

  54. [54]

    R. C. Walker:The Stone-Čech Compactification, Springer-Verlag, 1974. 28

    1974