I am working on a translation from French about, ultimately, the axiom of constructibility. In the opening paragraphs, the author describes how we are going to assume the ZF axioms are consistent to create a stronger theory with this axiom. Then, he goes on to say that it is harmless to also assume that there is a transitive ZF model (a set model). Then, he continues by making a precise statement about this which I translated as "More precisely, the theory of Zermelo-Fraenkel, including the single binary predicate $\in$ admits an expansion of the theory with $\in$ to include a unary predicate $\tau$ with an axiom saying a there is a unique set which is transitive and a ZF model by checking with $\tau$." I'm not sure if I got it right, so my question is:


How do you expand a model of ZF + the axiom of consistency to include that the model is transitive by adding a unary predicate? 



Assuming a transitive set model of ZF
Most likely the author is referring to the following fact:


The Reflection Scheme proves each instance of the following scheme: Let $\Delta$ be a finite subset of the axioms of ZF. ZF proves that there is a transitive set which is a model of $\Delta$.


Let $\tau$ be a constant symbol, and assume ZF is consistent. By the compactness theorem, there is a model of the following set of sentences:


ZF $\cup$ $\bigcup$ { $\tau$ is a transitive model of $\Delta$ : $\Delta$ is a finite subset of ZF }.


Note that $\tau$ is asserted to be a transitive model of ZF via a *scheme*. The single statement that there exists a transitive model of ZF has (much) greater consistency strength than CON(ZF), by considerations having to do with Gödel's second incompleteness theorem, plus absoluteness of arithmetical statements for transitive models.


