Tarskian truth theories over set theory

Ali Enayat

arxiv: 2604.03825 · v4 · pith:SYYRNUMGnew · submitted 2026-04-04 · 🧮 math.LO

Tarskian truth theories over set theory

Ali Enayat This is my paper

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.