Is ZFC plus a truth predicate capable of variable substitution consistent?

Question

Let us define a truth predicate that allows one to substitute in variables. For example, for a 3-ary predicate $p$ and sets $A$, $B$, and $C$, then $\text{true}(\ulcorner p \urcorner, A, B, C)$ (where $\ulcorner \cdot \urcorner$ is some sort of Godel numbering) is true if and only if $p(A, B, C)$ is true.

In particular, we define an axiom schema as follows: For every n-ary predicate $p$ in the language of (first-order) set theory $p$, we define an axiom $$\forall x_1x_2\dots x_n(p(x_1,x_2,\dots,x_n) \iff \text{true}(\ulcorner p \urcorner,x_1,x_2,\dots,x_n))$$

My question, is this schema plus the axioms of ZFC consistent (or rather, it is known to be inconsistent)?

My ideas so far:

• My first idea was to prove it inconsistent by turning $\text{true}$ into a set. Then you could substitute the truth predicate itself into arbitrary predicates, allowing us to apply Tarski's undefinability theorem. There is a set of true $0$-ary predicates (i.e. statements), namely $\{x|x \in \text{set of syntactically valid statements}, \text{true(x)}\}$ (this means that this theory can express the truthiness of statements in the language set theory plus an ordinary truth predicate). The problem is that we can not turn $true$ into a set for any an arity greater 1, since it would contain $(p(x):x=x, A)$ for all sets $A$, so it would be a class instead.

• Since in the last paragraph I showed that this theory could express the truthiness of set theory+regular truth predicate, my next idea was that we could show that it was equivalent to that theory (allowing us to apply the undefinability theorem). I have not been able to do this yet though.

• I'm not very good at showing proving consistency (or rather, showing relative consistency), so I don't have any ideas in that department.

Edit:

• Actually, we only need $\text{true}$ to work on 1-ary predicates, since any n-ary predicate can be converted to a 1-ary predicate that works on n-tuples.

Answer 1

The usual conception of truth predicate, or satisfaction class, is formulated in the way that you describe, allowing arguments. It doesn't handle only sentences (no free variables), but formulas, with free variables that can be evaluated as one likes.

Namely, a truth predicate is a class $T$ consisting of pairs $\langle\ulcorner\phi\urcorner,\vec a\rangle$, where $\vec a$ is a mapping of the free variables of $\phi$ to the objects listed by $\vec a$, in such a way that the Tarskian recursive definition of truth is obeyed. Namely,

• $T$ asserts atomic truths correctly.
• $T$ performs Boolean logic correctly, so that $T(\langle\ulcorner\neg\phi\urcorner,\vec a\rangle)$ holds just in case $T(\langle\ulcorner\phi\urcorner,\vec a\rangle)$ does not; and $T(\langle\ulcorner\phi\wedge\psi\urcorner,\vec a\rangle)$ holds just in case both $T(\langle\ulcorner\phi\urcorner,\vec a\rangle)$ and $T(\langle\ulcorner\psi\urcorner,\vec a\rangle)$ hold.
• $T$ performs quantifier logic correctly, so that $T(\langle\ulcorner\exists x\ \phi(x)\urcorner,\vec a\rangle)$ holds just in case there is some $b$ so that $T(\langle\ulcorner\phi\urcorner,b^\frown\vec a\rangle)$ holds.

In short, a truth predicate is a class that fulfills Tarski's recursive definition of truth. This implies every instance of your scheme, by induction on formulas.

Tarski's non-definability theorem says that such a class $T$ can never be definable, because if it were definable, we could in the Gödelian manner form a sentence that asserted its own non-truth, which would lead to contradiction.

But there is nothing wrong with having such a truth predicate as a non-definable class, and indeed the existence of such a truth predicate is provable in Kelley-Morse set theory and many other second-order set theories. See for example my post, Kelley-Morse proves Con(ZFC) and much more. Indeed, one can prove the existence of a truth predicate in $\text{GBC}+\text{ETR}_\omega$, which is the principle of elementary transfinite recursion of length $\omega$, allowing the definitions of classes by recursions of length $\omega$. Truth itself is defined by recursion on formulas, and so this principle is enough to get the truth predicate. (But strictly stronger, since $\text{ETR}_\omega$ allow class parameters, and so one gets truth-about-truth this way, but no such predicate could be definable from a truth predicate.)

Let me add that the particular way you have expressed your axiom is much weaker than having a truth predicate, and it does not have any consistency strength at all. You haven't required your "true" predicate to obey the Tarskian recursion, but only that it gets the right answer on any particular formula/argument pair. One can easily show that this weak theory is consistent by a simple compactness argument. Namely, for any model $M\models\text{ZFC}$ consider the theory $T$ in the language with an additional predicate "true" asserting the elementary diagram of $M$ (all truths of $M$ with constants for every element) plus the assertion that "true" has all the statements in your scheme, of any particular predicate $p$. This theory is finitely consistent, since for any finitely many predicates, we can easily define a partial truth predicate that covers them. So the theory is consistent, and any model of the theory provides an elementary extension of $M$, with all the same truths of $M$, but which also has your desired truth predicate.

Although this shows that your theory is equiconsistent with ZFC, it also shows that you haven't stated everything that you want for the "true" predicate, since there is no way to prove in this theory that "true" is defined on all formulas, because the axioms only ensure that it is defined on standard formulas. Indeed, in a model of $\neg\text{Con}(ZFC)$, it cannot be defined on all formulas and obey the Tarskian recursion, since the existence of a truth predicate in the Tarskian sense implies $\text{Con}(ZFC)$.

Finally, another issue to consider with respect to truth predicates is the extent to which they may figure as parameters in the other axioms. For example, if we augment ZFC set theory with a truth predicate $T$, then this won't be so useful unless we also allow $T$ to appear as a class parameter in the replacement axioms. That is, we want to have ZFC(T), allowing ourselves to use $T$ just as we would use any class. Such a class is said to be strongly amenable, and so what we really want is not just a truth predicate, but a strongly amenable truth predicate. Thus, one should really add those additional axioms, which amounts to working in GBc rather than ZFC. (In arithmetic, one speaks of an inductive truth predicate, which is a truth predicate that is allowed to appear in instances of the induction axiom.)