[FOM] The semantics of set theory

[Richard Heck]

Ralf Schindler wrote:

 >For any fixed concrete integer n>0, the formula "x is a true \Sigma_n
 >sentence of set theory" can be written as a \Sigma_n formula of set
 >theory; ZF proves every relevant instance of the Tarski schema.
 >Therefore, the formula "x is a true sentence of set theory" can be 
 >written as a \Sigma_1 (!) formula of class theory (by saying "there is 
 >a class containing only truths to which x belongs"); BG proves every 
 >instance of the Tarski schema....

The situation here is analogous to that with PA, isn't it? In PA, we can
define "x is a true \Sigma_n sentence of PA" as a \Sigma_n sentence of
PA and prove the Tarski-conditions for \Sigma_n sentences. (Actually, it
can all be done for satisfaction, but that complicates the statement of
the result in inessential ways.) In predicative second-order PA, we can
then define a truth-predicate for (first-order) sentences of PA and
prove the Tarski-conditions. But then we cannot treat truth, so defined,
as itself a "property". Comprehension will not apply to that formula, so
the usual sort of trivial induction one uses to prove consistency in an
oridinary truth-theory for PA doesn't work. More generally, although one
can prove the Tarski-conditions, one can not use them to prove many
interesting generalizations about truth, because such proofs typically
proceed by induction on the complexity of expressions. Further, there
are various results equating the strength of these sorts of theories
with axiomatic truth-theories for PA in which 'true' is not allowed to
occur in the induction axioms.

OK. So how deep does the analogy go? How much of what's just been said
about PA is true of the situation with ZFC? To what extent do these
results apply in general? I'm guessing Ralf knows the answers to these
questions.

Best to all,
Richard Heck