A truth predicate for first order set theory would allow you to determine the truth of statements in first order set theory. A definition is given [here](https://mathoverflow.net/a/273121/65915).


My question is, can you formulate a statement or axiom asserting that such a truth predicate does *not* exist.


In particular, a truth predicate would need to be an undefinable proper class, and so can not be quantified over in first order set theory. In general, if we could somehow create a statement saying there is no truth predicate, we could negate it, use [existential instantiation](https://en.wikipedia.org/wiki/Existential_instantiation), and then [Tarski's undefinability theorem](https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem) to arrive at a paradox.


Now, we can work in a stronger language which supports classes, but doing so (when you add suitable axioms for working with the new language) often implies the existence of a truth predicate. For example [Kelly-Morse set theory](https://en.wikipedia.org/wiki/Morse%E2%80%93Kelley_set_theory) [does](http://jdh.hamkins.org/km-implies-conzfc/).


Can we formulate such an axiom?


(The purpose of this is so I can formulate the philosophy mathematical nonrealism mathematically, so as to show it meaningless by its own principles (half jokingly)).



Can you formulate a theory stating that a truth predicate does not exist for first order set theory?
The assertion that there is (or is not) a truth predicate is expressible in the second-order language of set theory, but assuming consistency, not by any first-order assertion. 


**Second-order.** In the second-order case, one simply says that there is a class $T$ satisfying the Tarskian recursion $$\exists T\ (T\text{ is a truth predicate}).$$ I gave the detailed definition of what it means to say that a class $T$ is a truth predicate in [my answer to your other question](https://mathoverflow.net/a/273121/1946), to which you linked, and those properties constitute a finite conjunction of first-order properties of $T$. So to say that there is a truth predicate involves a single second-order quantifier $\exists T$. 


It follows of course that the non-existence of such a predicate is also expressible, using $$\neg\exists T\ (T\text{ is a truth predicate}).$$ 
This is a $\Pi^1\_1$ assertion in the second-order language of set theory.


The theory GBC+"there is no truth predicate" is equiconsistent with ZFC, since clearly the consistency of this theory implies the consistency of ZFC, and conversely, if there is a model of ZFC, then there is a model of GBC having only definable classes, and this model has no truth predicate. So the assertion that there is no truth has no large-cardinal consistency strength. 


In contrast, the assertion that there *is* a truth predicate does transcend ZFC in consistency strength, since it implies Con(ZFC) and Con(Con(ZFC)) and much more, as I explain in [my blog post](http://jdh.hamkins.org/km-implies-conzfc/), to which you linked. 


**First-order.** Meanwhile, I claim that the assertion that there is (or is not) a truth predicate, if consistent, is not expressible by any first-order assertion in the language of set theory, and perhaps this is the answer to your question. 


**Theorem.** If GBC+$\exists$ truth-predicate is consistent, then there is no first-order assertion that GBC proves to be equivalent to the existence of a truth-predicate. 


**Proof.** Let $(M,\in^M,S)$ be a model of GBC with a truth predicate. We may assume $M$ has a definable global well-order, by going to $L^M$ if necessary. Let $M\_0=(M,\in^M,\text{Def}(M))$ be the smaller model of GBC having only definable classes. Since $M$ and $M\_0$ have the same first-order objects, they satisfy all the same first-order assertions. But $M$ has a truth-predicate and $M\_0$ does not. So the assertion that there is a truth predicate cannot be first-order expressible. $\Box$


**Theorem.** The theory GBC + "there is no truth predicate for first-order truth" is conservative over GBC and hence also over ZFC for first-order assertions. That is, the theory proves no new statements about sets.


**Proof.** Any model of ZFC can be extended to a model of GBC with the same sets, but having no truth predicate. (One needs to check that forcing to add a global well-order does not add a truth predicate, but one can do this by appealing to the homogeneity of this forcing.) Thus, any statement that holds in some model of ZFC also holds in some model of GBC + "there is no truth predicate", and so this theory has no new consequences for sets. $\Box$


Lastly, let me mention that the truth predicate, when it exists, although it is not first-order definable, is nevertheless first-order *implicitly definable* (and hence first-order algebraic), since when it exists it is the unique class with that first-order property. (See more about this concept of implicit definability and algebraicity in my paper: *Hamkins, Joel David; Leahy, Cole*, [**Algebraicity and implicit definability in set theory**](http://jdh.hamkins.org/algebraicity-and-implicit-definability/), Notre Dame J. Formal Logic, vol. 57, iss. 3, pp. 431-439, 2016. [doi:10.1215/00294527-3542326](http://dx.doi.org/10.1215/00294527-3542326), [ZBL06621300](https://zbmath.org/?q=an:06621300).)


