pith. sign in

arxiv: 1907.08368 · v1 · pith:QHQOVGJ4new · submitted 2019-07-18 · 💻 cs.LO

A Tale of Two Set Theories

Chad E. Brown , Karol P\k{a}k This is my paper

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

classification 💻 cs.LO
keywords Tarski-Grothendieck set theoryMizarEgalTarski's Axiom AGrothendieck universeformal verificationhigher-order logicfirst-order logic
0
0 comments X

The pith

Two versions of Tarski-Grothendieck set theory, one first-order in Mizar and one higher-order in Egal, are shown to support each other's central axiom and primitive via equivalent presentations.

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

The paper examines the relationship between the first-order Tarski-Grothendieck set theory used in Mizar and the higher-order version used in Egal. It establishes that certain higher-order terms and propositions in Egal have direct first-order counterparts in Mizar. Using these correspondences, the authors prove Tarski's Axiom A inside Egal and construct a Grothendieck Universe operator inside Mizar. This cross-system work demonstrates that the two formalizations can exchange their distinctive foundational elements.

Core claim

By showing how higher-order terms in Egal have equivalent first-order presentations in Mizar, Tarski's Axiom A is proved in Egal and a Grothendieck Universe operator satisfying its axioms is constructed in Mizar.

What carries the argument

Equivalent presentations that translate higher-order terms and propositions from Egal into first-order statements in Mizar, enabling the transfer of axioms and operator constructions between the systems.

If this is right

  • Egal gains the ability to express and prove the full strength of Tarski's Axiom A as used in Mizar.
  • Mizar gains an explicit Grothendieck Universe operator with its defining axioms as a defined construction rather than a primitive.
  • Many set-theoretic statements can be moved between the two systems while retaining their logical status.

Where Pith is reading between the lines

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

  • Proofs developed in one system could be mechanically ported to the other once the translations are automated.
  • The result suggests that the choice between first-order and higher-order presentations of Tarski-Grothendieck set theory is less absolute than it first appears.

Load-bearing premise

The translations between higher-order terms in Egal and their first-order presentations in Mizar preserve the intended meaning of the set-theoretic statements.

What would settle it

A concrete higher-order statement in Egal whose first-order translation in Mizar is provable in one system but not the other, or requires axioms absent from the target system.

Figures

Figures reproduced from arXiv: 1907.08368 by Chad E. Brown, Karol P\k{a}k.

Figure 1
Figure 1. Figure 1: Tarski’s Axiom A in Mizar FOTG was not the only foundation considered for the library. One of the main reasons it was chosen is the usefulness of Axiom A in the formalization of category theory. Namely, FOTG provides many universes that have properties analogous to those of a class of all sets. In particular, every axiom of ZFC remains true if we relativize quantifiers to the given universe. The axiom of c… view at source ↗
Figure 2
Figure 2. Figure 2: Natural deduction sytem We now briefly discuss the role of polymorphism in Egal. We have already seen examples where type variables would be useful. Instead of having infinitely many constants εσ in the implementation there is one constant ε which must be associated with a type when used. Likewise, the axioms of functional extension￾ality and choice make use of type variables and whenever these axioms are … view at source ↗
read the original abstract

We describe the relationship between two versions of Tarski-Grothendieck set theory: the first-order set theory of Mizar and the higher-order set theory of Egal. We show how certain higher-order terms and propositions in Egal have equivalent first-order presentations. We then prove Tarski's Axiom A (an axiom in Mizar) in Egal and construct a Grothendieck Universe operator (a primitive with axioms in Egal) in Mizar.

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

Summary. The manuscript describes the relationship between two versions of Tarski-Grothendieck set theory: the first-order set theory of Mizar and the higher-order set theory of Egal. It shows how certain higher-order terms and propositions in Egal have equivalent first-order presentations. It then proves Tarski's Axiom A (an axiom in Mizar) in Egal and constructs a Grothendieck Universe operator (a primitive with axioms in Egal) in Mizar.

Significance. If the formalizations hold, the work supplies explicit machine-checked proofs of key cross-system constructions together with a syntactic translation between the two presentations. This provides a concrete, verifiable bridge between a first-order and a higher-order formalization of the same set theory, which is a strength for reproducibility and for understanding how axioms and operators transfer between proof assistants.

major comments (1)
  1. [section on equivalent presentations] Section on equivalent presentations: the claim that the translations preserve the intended meaning of the set-theoretic statements rests on direct syntactic correspondence between higher-order terms in Egal and first-order presentations in Mizar. No separate soundness or conservativity argument is supplied to confirm that the correspondence is faithful for the statements involved in the subsequent constructions; this is load-bearing for the relationship asserted between the two systems.
minor comments (1)
  1. The manuscript states that the proofs and constructions were performed inside the respective assistants, but does not include or link to the actual formal code; adding such links would improve verifiability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and the positive recommendation for minor revision. We address the single major comment below.

read point-by-point responses

  1. Referee: Section on equivalent presentations: the claim that the translations preserve the intended meaning of the set-theoretic statements rests on direct syntactic correspondence between higher-order terms in Egal and first-order presentations in Mizar. No separate soundness or conservativity argument is supplied to confirm that the correspondence is faithful for the statements involved in the subsequent constructions; this is load-bearing for the relationship asserted between the two systems.

    Authors: The section on equivalent presentations defines the translations explicitly by direct syntactic correspondence, chosen so that the higher-order terms in Egal and their first-order renderings in Mizar express the same set-theoretic content by construction. These are not advanced as a general soundness or conservativity theorem between the two systems; rather, they serve as concrete bridges for the specific statements required to carry out the subsequent formal work. The machine-checked proofs that Tarski's Axiom A holds in Egal and that a Grothendieck-universe operator exists in Mizar then verify the relationship inside each assistant. We will insert a short clarifying paragraph in the revised version to make this scope explicit and to note that no additional meta-theoretic justification is claimed or required for the constructions presented. revision: partial

Circularity Check

0 steps flagged

No significant circularity; direct formal constructions

full rationale

The paper's central results are explicit machine-checked proofs (Tarski Axiom A inside Egal; Grothendieck-universe operator inside Mizar) together with a direct syntactic translation between higher-order and first-order presentations. These steps are carried out inside the respective proof assistants and do not reduce to fitted parameters, self-definitional equations, or load-bearing self-citations whose validity depends on the present work. The translation is syntactic correspondence rather than an external semantic argument that would require prior results from the same authors. No step matches any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper works inside the existing axiom systems of Mizar and Egal; it introduces no new free parameters, no new invented entities, and relies only on standard mathematical logic axioms plus the Tarski-Grothendieck axioms already present in both systems.

axioms (2)
  • standard math Standard axioms of first-order logic and higher-order logic as implemented in Mizar and Egal
    Invoked throughout as the background logic for both systems.
  • domain assumption Tarski-Grothendieck set theory axioms
    The common foundation whose two presentations are being related.

pith-pipeline@v0.9.0 · 5592 in / 1359 out tokens · 20986 ms · 2026-05-24T19:40:44.837007+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

25 extracted references · 25 canonical work pages

  1. [1]

    Formalized Mat hematics 1(3), 563–567 (1990)

    Bancerek, G.: Tarski’s Classes and Ranks. Formalized Mat hematics 1(3), 563–567 (1990)

    work page 1990

  2. [2]

    Formal ized Mathematics 1(2), 265–267 (1990)

    Bancerek, G.: Zermelo Theorem and Axiom of Choice. Formal ized Mathematics 1(2), 265–267 (1990)

    work page 1990

  3. [3]

    Mizar: State-of-the-art and beyond

    Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Nau- mowicz, A., Pąk, K., Urban, J.: Mizar: State-of-the-art and Beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intell igent Computer Math- ematics - International Conference, CICM 2015. LNCS, vol. 9 150, pp. 261–279. Springer (2015). https://doi.or...

    work page doi:10.1007/978-3-319-20615-8_17 2015

  4. [4]

    Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Nau- mowicz, A., Pąk, K.: The Role of the Mizar Mathematical Libra ry for Interac- tive Proof Development in Mizar. J. Autom. Reasoning 61(1–4), 9–32 (2018). https://doi.org/10.1007/s10817-017-9440-6 16 Chad E. Brown, Karol Pąk

    work page doi:10.1007/s10817-017-9440-6 2018

  5. [5]

    Royal Society of London Transactions Series A 363, 2351–2375 (2005)

    Barendregt, H., Wiedijk, F.: The challenge of computer ma thematics. Royal Society of London Transactions Series A 363, 2351–2375 (2005)

    work page 2005

  6. [6]

    In: Mohamed, O.A

    Bertot, Y.: A Short Presentation of Coq. In: Mohamed, O.A. , Muñoz, C.A., Tahar, S. (eds.) Theorem Proving in Higher Orde r Log- ics (TPHOLs 2008). LNCS, vol. 5170, pp. 12–16. Springer (200 8). https://doi.org/10.1007/978-3-540-71067-7_3

    work page doi:10.1007/978-3-540-71067-7_3 2008

  7. [7]

    Brown, C.E.: The Egal manual (Sep 2014)

    work page 2014

  8. [8]

    Brown, C.E.: Reconsidering Pairs and Functions as Sets. J . Autom. Reasoning 55(3), 199–210 (Oct 2015). https://doi.org/10.1007/s10817-015-9340-6

    work page doi:10.1007/s10817-015-9340-6 2015

  9. [9]

    Brown, C.E., Pąk, K.: A tale of two set theories (2019), http://alioth.uwb.edu.pl/~pakkarol/publications.html

    work page 2019

  10. [10]

    T he Journal of Symbolic Logic 5, 56–68 (1940)

    Church, A.: A Formulation of the Simple Theory of Types. T he Journal of Symbolic Logic 5, 56–68 (1940)

    work page 1940

  11. [11]

    Pr oceedings of the Amer- ican Mathematical Society 51, 176–178 (1975)

    Diaconescu, R.: Axiom of Choice and Complementation. Pr oceedings of the Amer- ican Mathematical Society 51, 176–178 (1975)

    work page 1975

  12. [12]

    Fundamenta Mathematicae 71(1), 43–62 (1971)

    Felgner, U.: Comparison of the Axioms of Local and Univer sal Choice. Fundamenta Mathematicae 71(1), 43–62 (1971)

    work page 1971

  13. [13]

    North-Holland Pub

    Fraenkel, A.A., Bar-Hillel, Y., Lévy, A.: Foundations o f Set Theory. North-Holland Pub. Co (1973)

    work page 1973

  14. [14]

    (ed s.) Theorem Proving in Higher Order Logics

    Gordon, M.: Set Theory, Higher Order Logic or Both? In: Go os, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (ed s.) Theorem Proving in Higher Order Logics. pp. 191–201. Springer Berlin Heidelbe rg, Berlin, Heidelberg (1996). https://doi.org/10.1007/BFb0105405

    work page doi:10.1007/bfb0105405 1996

  15. [15]

    Journal of Formalized Reasoning 3(2), 153–245 (2010)

    Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a Nutshell. Journal of Formalized Reasoning 3(2), 153–245 (2010)

    work page 2010

  16. [16]

    Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four Dec ades of Mizar. J. Autom. Reasoning 55(3), 191–198 (2015). https://doi.org/10.1007/s10817-015-9345-1

    work page doi:10.1007/s10817-015-9345-1 2015

  17. [17]

    1, Lecture Notes in Mathematics, vol

    Grothendieck, A., Verdier, J.L.: Théorie des topos et co homologie étale des schémas - (SGA 4) - vol. 1, Lecture Notes in Mathematics, vol. 269. Spr inger-Verlag (1972)

    work page 1972

  18. [18]

    Studia Logi ca 1 (1934)

    Jaśkowski, S.: On the Rules of Suppositions. Studia Logi ca 1 (1934)

    work page 1934

  19. [19]

    In: Geuvers, H., England, M., Hasa n, O., Rabe, F., Teschke, O

    Kaliszyk, C., Pąk, K.: Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic. In: Geuvers, H., England, M., Hasa n, O., Rabe, F., Teschke, O. (eds.) Intelligent Computer Mathematics - 1 0th International Conference, CICM 2017. LNCS, vol. 10383, pp. 193–207. Sprin ger (2017). https://doi.org/10.1007/978-3-319-62075-6_14

    work page doi:10.1007/978-3-319-62075-6_14 2017

  20. [20]

    Kaliszyk, C., Pąk, K.: Semantics of Mizar as an Isabelle o bject logic. J. Autom. Reasoning (2018). https://doi.org/10.1007/s10817-018-9479-z

    work page doi:10.1007/s10817-018-9479-z 2018

  21. [21]

    Kirst, D., Smolka, G.: Categoricity Results and Large Mo del Constructions for Second-Order ZF in Dependent Type Theory. J. Autom. Reasoni ng (2018). https://doi.org/10.1007/s10817-018-9480-6, first Online: 11 October 2018

    work page doi:10.1007/s10817-018-9480-6 2018

  22. [22]

    Formalized Mathematics 1(3), 595– 600 (1990)

    Nowak, B., Bancerek, G.: Universal Classes. Formalized Mathematics 1(3), 595– 600 (1990)

    work page 1990

  23. [23]

    In: Barkaou i, K., Cavalcanti, A., Cerone, A

    Obua, S.: Partizan Games in Isabelle/HOLZF. In: Barkaou i, K., Cavalcanti, A., Cerone, A. (eds.) Theoretical Aspects of Computing - ICT AC 2006. LNCS, vol. 4281, pp. 272–286. Springer (2006). https://doi.org/10.1007/11921240_19

    work page doi:10.1007/11921240_19 2006

  24. [24]

    Fundam enta Mathematicae 30, 68–89 (1938)

    Tarski, A.: Über Unerreichbare Kardinalzahlen. Fundam enta Mathematicae 30, 68–89 (1938)

    work page 1938

  25. [25]

    Journal o f Formalized Mathematics Axiomatics (2002), released 1989

    Trybulec, A.: Tarski Grothendieck Set Theory. Journal o f Formalized Mathematics Axiomatics (2002), released 1989

    work page 2002