arxiv: 2604.03825 · v3 · submitted 2026-04-04 · 🧮 math.LO

Recognition: 2 theorem links

· Lean Theorem

Tarskian truth theories over set theory

Ali Enayat

Authors on Pith no claims yet

Pith reviewed 2026-05-13 16:56 UTC · model grok-4.3

classification 🧮 math.LO

keywords Tarskian truthtruth theoriesKripke-Platek set theoryZermelo-Fraenkel set theorymodel theoryproof theoryaxiomatic truth

0 comments

The pith

Model-theoretic methods establish new proof-theoretic theorems for Tarskian truth theories over KP and ZF set theory.

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

The paper applies model-theoretic constructions to derive fresh proof-theoretic results for axiomatic theories that add a truth predicate to base set theories including Kripke-Platek set theory and Zermelo-Fraenkel set theory. These truth theories satisfy the Tarskian biconditionals that define truth for each sentence in the language. A sympathetic reader cares because the results clarify the consistency strength and interpretability relations between truth axioms and set-theoretic axioms. The work relies on building models that satisfy both the set theory and the truth axioms simultaneously rather than working directly with formal proofs.

Core claim

Axiomatic Tarskian truth theories over KP and stronger set theories like ZF admit model-theoretic constructions that establish new proof-theoretic theorems about their relative consistency and strength.

What carries the argument

Model-theoretic constructions that expand models of the base set theory KP or ZF to include a truth predicate satisfying the Tarskian biconditionals.

If this is right

The combined truth-set theories are consistent relative to the consistency of the base set theory.
New bounds on the proof-theoretic strength of these systems follow from the model constructions.
Interpretability relations among different axiomatic truth theories over the same set theory are established.

Where Pith is reading between the lines

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

The same model constructions might extend to set theories stronger than ZF such as those with large cardinals.
If the methods apply more broadly they could relate truth theories to questions of definability in set theory.

Load-bearing premise

Suitable models of the base set theories exist that can be expanded to satisfy the added truth axioms.

What would settle it

A demonstration that a claimed model for one of the truth-set theory combinations fails to exist or that a specific consistency statement does not hold would refute the theorems.

read the original abstract

This work uses mostly model-theoretic methods to establish new proof-theoretic theorems about several axiomatic theories of truth over KP (Kripke-Platek set theory) and stronger theories, especially ZF (Zermelo-Fraenkel set theory).

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.

Desk Editor's Note private letter to a colleague

Enayat's work provides new proof-theoretic theorems about Tarskian truth theories over KP and ZF using model-theoretic methods.

read the letter

The punchline is that Enayat has some new proof-theoretic theorems for Tarskian truth theories built over KP and ZF, obtained mostly through model-theoretic constructions. The paper takes several axiomatic systems that extend KP or ZF with a truth predicate obeying the usual Tarskian compositional axioms and derives results about their strength. This includes things like relative consistency or what they can prove. The model-theoretic approach involves constructing models of the base set theory that can be expanded to satisfy the truth axioms without increasing the overall strength in unwanted ways. This is a standard move in the field but applied here to get fresh results at the ZF level. What it does well is the careful handling of the stronger base theory. Much of the literature on truth theories is over arithmetic or KP, so moving to ZF is a step forward. The methods appear to be applied cleanly, with no obvious circularity or invented assumptions. The abstract claims new theorems, and the stress test found no internal inconsistencies in the approach. Soft spots are limited. The model constructions rely on the existence of suitable models for KP and ZF, which is fine given the consistency assumptions, but the paper would benefit from explicit checks that the truth axioms don't interfere with the set-theoretic properties in subtle ways. Model theory gives existence results but can leave the exact proof-theoretic characterization a little less direct than a purely syntactic analysis would. These are normal for the method and not deal breakers. This paper is for logicians working on truth theories in set theory or proof theory of strong systems. Someone who follows work on Kripke-Feferman truth or similar over set bases will find the new theorems relevant and worth checking against their own results. It deserves a serious referee because the claims are specific, the methods are appropriate, and the topic has ongoing interest in the subfield. I recommend putting it through peer review.

Referee Report

2 major / 2 minor

Summary. The paper uses model-theoretic constructions to establish new proof-theoretic results for several Tarskian (compositional) truth theories formulated over Kripke-Platek set theory (KP) and stronger base theories, in particular Zermelo-Fraenkel set theory (ZF). It proves consistency, interpretability, and ordinal-analysis statements for the resulting truth extensions.

Significance. If the central claims hold, the work meaningfully extends the model-theoretic treatment of truth theories from weaker arithmetical or KP bases to full ZF, supplying concrete consistency-strength calibrations and conservation results that were previously unavailable. The explicit use of model-theoretic methods to obtain proof-theoretic conclusions is a clear strength.

major comments (2)

[§4.2, Theorem 4.7] §4.2, Theorem 4.7: the argument that the truth predicate satisfies the full Tarskian compositional axioms in the constructed model relies on the base theory proving the existence of a satisfaction class for the language with the truth predicate; this step is only sketched and appears to require an additional global choice or reflection assumption not stated in the theorem hypothesis.
[§5.3, Corollary 5.12] §5.3, Corollary 5.12: the claimed proof-theoretic ordinal for the truth theory over ZF is stated as Γ₀, but the reduction to the base theory's ordinal analysis is not carried out in detail; the model-theoretic construction controls consistency but does not obviously yield the exact ordinal bound without an additional cut-elimination or ordinal-notation argument.

minor comments (2)

[§2] Notation for the truth predicate is introduced in §2 but then used with varying subscripts (T, Tr, Sat) without a single consolidated table; this makes cross-references in later sections harder to follow.
[Abstract and §6] The abstract claims 'mostly model-theoretic methods,' yet §6 contains a non-trivial amount of syntactic conservativity arguments; a brief clarification of the division of labor would help.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We address each major point below and will revise the manuscript accordingly to improve clarity and detail.

read point-by-point responses

Referee: [§4.2, Theorem 4.7] the argument that the truth predicate satisfies the full Tarskian compositional axioms in the constructed model relies on the base theory proving the existence of a satisfaction class for the language with the truth predicate; this step is only sketched and appears to require an additional global choice or reflection assumption not stated in the theorem hypothesis.

Authors: The model construction in Theorem 4.7 proceeds entirely within the resources of the base theory (KP or ZF) and does not invoke global choice or extra reflection. The existence of the required satisfaction class follows from the inductive definition of the model and the base theory's ability to handle satisfaction for the expanded language, as already established in Lemma 4.5. We will expand the sketch in the revised version with a fully explicit verification of the compositional clauses, citing the precise base-theory facts used. revision: partial
Referee: [§5.3, Corollary 5.12] the claimed proof-theoretic ordinal for the truth theory over ZF is stated as Γ₀, but the reduction to the base theory's ordinal analysis is not carried out in detail; the model-theoretic construction controls consistency but does not obviously yield the exact ordinal bound without an additional cut-elimination or ordinal-notation argument.

Authors: The model-theoretic construction yields an interpretation of the truth theory into a conservative extension of the base theory whose proof-theoretic ordinal is known to be Γ₀. This supplies the exact bound once the interpretation is combined with the base theory's ordinal analysis. We agree the reduction step is only indicated rather than fully written out. In the revision we will insert a short subsection that spells out the embedding and the appeal to the known cut-elimination result for the base theory. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper applies standard model-theoretic methods to obtain proof-theoretic results for Tarskian truth theories over KP and ZF. No equations, definitions, or constructions reduce by construction to fitted inputs, self-referential axioms, or load-bearing self-citations. The abstract and description indicate independent use of established techniques without any renaming of known results or smuggling of ansatzes via prior work by the same authors. The central claims rest on external model existence and compositional truth axioms whose applicability is not internally forced by the target theorems.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Only the abstract is available, so the ledger records the standard background assumptions of the field rather than paper-specific details.

axioms (2)

domain assumption Axioms of Kripke-Platek set theory (KP)
The paper builds truth theories over KP as the base theory.
domain assumption Axioms of Zermelo-Fraenkel set theory (ZF)
Stronger base theory used for comparison and extension.

pith-pipeline@v0.9.0 · 5309 in / 1110 out tokens · 23929 ms · 2026-05-13T16:56:19.522102+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Theorem A: CT∗[ZF], CT−[ZF]+Int-Repl+DCout, CT−[ZF]+Int-Ref have same deductive closure
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat ≃ Nat recovery unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Theorem D: CT−[ZF]+Coll(T) conservative over ZF

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

15 extracted references · 15 canonical work pages

[1]

Beklemishev and F

[BP] L. Beklemishev and F. Pakhomov,Reflection algebras and conservation results for theories of iterated truth,Annals of Pure and Applied Logic,vol. 173(5), 103093 (2022), 41 pp. [BBJ] G. Boolos, J. Burgess, and R. Jeffrey,Computability and logic, Fifth edition. Cambridge University Press, Cambridge,

work page 2022
[2]

Cie´ sli´ nski,Deflationary Truth and Pathologies,Journal of Philosophical Logic, vol

[C-1] C. Cie´ sli´ nski,Deflationary Truth and Pathologies,Journal of Philosophical Logic, vol. 39 (2010), pp. 325–337. [C-2] C. Cie´ sli´ nski,The Epistemic Lightness of Truth:Deflationism and its Logic, Cambridge University Press, Cambridge,

work page 2010
[3]

Cie´ sli´ nski,On some problems with truth and satisfaction, inPhilosophical Approaches to the Foundations of Logic and Mathematics (ed

[C-3] C. Cie´ sli´ nski,On some problems with truth and satisfaction, inPhilosophical Approaches to the Foundations of Logic and Mathematics (ed. M. Trepczy´ nski), pp. 175–192, Brill (2021). [C LW] C. Cie´ sli´ nski, M. Le lyk, and B. Wcis lo,The two halves of disjunctive correctness,Jounal of Mathematical Logic, vol. 23(2), Article no. 2250026, (2023), ...

work page 2021
[4]

Enayat,Models of set Theory with definable ordinals,Archive for Mathematical Logic, vol

[E-1] A. Enayat,Models of set Theory with definable ordinals,Archive for Mathematical Logic, vol. 44 (2005), pp. 363–385. [E-2] A. Enayat,Satisfaction classes with approximate disjunctive correctness,Review of Symbolic Logic,vol. 18 (2025), 545–562. [E-3] A. Enayat,The Mostowski Bridge(2025),arXiv:2505.23998. 38 [E L] A. Enayat and M. Le lyk,Axiomatizatio...

work page arXiv 2005
[5]

Felgner,Choice functions on sets and classes, in: Sets and Classes (on the Work by Paul Bernays), in: Studies in Logic and the Foundations of Math., vol

[Fel] U. Felgner,Choice functions on sets and classes, in: Sets and Classes (on the Work by Paul Bernays), in: Studies in Logic and the Foundations of Math., vol. 84, North-Holland, Amsterdam, 1976, pp. 217–255. [Fi] M. Fischer,Truth and speed-up,The Review of Symbolic Logic, vol. 7 (2014), pp. 319–340. [FLW] S. Friedman, W. Li, and T. L. Wong,Fragments o...

work page 1976
[6]

Fujimoto,Deflationism beyond arithmetic,Synthese(2019),vol

[Fu-2] K. Fujimoto,Deflationism beyond arithmetic,Synthese(2019),vol. 196, pp. 1045–1069. [HP] P. H´ ajek and P. Pudl´ ak,Metamathematics of First-Order Arithmetic, Springer,

work page 2019
[7]

Halbach, G

[HL L] V. Halbach, G. Leigh, and M. Le lyk,Axiomatic Theories of Truth,The Stanford Encyclopedia of Philosophy (Winter 2025 Edition), E. Zalta & U. Nodelman (eds.),https://plato.stanford.edu/archives/win2025/entries/truth-axiomatic/. [He] R.K. Heck,Some Remarks on ’Logical’ Reflection,PhilArchive(2025). [H-1] W. Hodges,Truth in a Structure,Proceedings of ...

work page 2025
[8]

Horsten, G

[HLR] L. Horsten, G. Luo, and S. Roberts,Truth and Finite Conjunction,Mind, vol. 133 (2024), pp. 1121–1135. [J] T. Jech,Set Theory, Springer Monographs in Mathematics, Springer, Berlin (2003). [KW] R. Kaye and T. Wong,On interpretations of arithmetic and set theory,Notre Dame Journal of Formal Logic, vol. 48, (2007), pp. 497–510. [KM] H. Keisler and M. Mo...

work page 2024
[9]

Kotlarski,Bounded induction and satisfaction classes,Mathematical Logic Quarterly.vol

[Kot] H. Kotlarski,Bounded induction and satisfaction classes,Mathematical Logic Quarterly.vol. 32 (1986), pp. 531–

work page 1986
[10]

Kotlarski, S

[KKL] H. Kotlarski, S. Krajewski, and A. H. Lachlan,Construction of satisfaction classes for nonstandard models,Cana- dian Mathematical Bulletin,vol. 24 (1981), pp. 283–293. [Kra] S. Krajewski,Nonstandard satisfaction classes, inSet Theory and Hierarchy Theory: A Memorial Tribute to Andrzej Mostowski(edited by W. Marek et al.) Lecture Notes in Mathematics...

work page 1981
[11]

Leigh,Conservativity for theories of compositional truth via cut elimination.Journal of Symbolic Logic, vol

[Lei] G. Leigh,Conservativity for theories of compositional truth via cut elimination.Journal of Symbolic Logic, vol. 80 (2015), 845–865. [ Le l] M. Le lyk,Model theory and proof theory of the global reflection principle,Journal of Symbolic Logic,vol. 88, 738–779,(2023). [Lev] A. Levy,A Hierarchy of Formulas in Set Theory, Memoirs of American Mathematical...

work page 2015
[12]

McKenzie,On the relative strengths of fragments of collection,Mathematical Logic Quarterly, vol

[McK] Z. McKenzie,On the relative strengths of fragments of collection,Mathematical Logic Quarterly, vol. 65 (2019), pp. 80–94. [Mat-1] A. Mathias,The strength of Mac Lane set theory,Annals of Pure and Applied Logic, vol. 110, (2001), pp. 107–234. 39 [Mat-2] A. Mathias,Weak systems of Gandy, Jensen and Devlin,Set theory, pp. 149–224, Trends Math., Birkh¨ ...

work page 2019
[13]

Montague,Fraenkel’s addition to the axioms of Zermelo, inLogic, Methodology and Philosophy of Science, Proceedings of the 1964 International Congress (ed

[Mon] R. Montague,Fraenkel’s addition to the axioms of Zermelo, inLogic, Methodology and Philosophy of Science, Proceedings of the 1964 International Congress (ed. by Bar-Hille), Jerusalem. Amsterdam, North-Holland,

work page 1964
[14]

Montague and R

[MV] R. Montague and R. Vaught,Natural models of set theories,Fund. Math.vol. 47 (1959), pp. 219–242. [Mos] A. Mostowski,Some impredicatve definitions in the axiomatic set-theory,Fundamenta Mathematicae,vol. 37 (1950), pp. 111-124. [Sh] J. Shoenfield,Mathematical Logic, Reprint of the 1973 second printing, Association for Symbolic Logic, Urbana, IL; A K P...

work page 1959
[15]

Tarski and R

[TV] A. Tarski and R. Vaught,Arithmetical extensions of relational systems,Compositio Mathematicavol. 13 (1957), pp. 81–102. [Va] R. Van Wesep,Satisfaction relations for proper classes: applications in logic and set theory,Journal of Symbolic Logic, vol. 78 (2013), pp. 345–368. [Vi] A. Visser,Pairs, sets and sequences in first-order theories,Archive for M...

work page 1957