[FOM] FOM: The semantics of set theory

[Volker Halbach]

Richard Heck asked about truth definition in predicative extensions of ZF 
and PA.

There are claims in the literature before 1950 (and even later) that you 
can prove consistency of a theory as soon as you have a truth predicate. 
Then Mostowski showed in the article "Some Impredicative Definitions in the 
Axiomatic Set-Theory" quoted by Ralf
that Bernays-Goedel set theory has a truth predicate for the language 
without class variables for which the T-sentences hold. BG, however, is 
conservative over ZF and therefore cannot prove the consistency of ZF.

As Richard noted, we have an analogous situation in arithmetic: If we add 
predicative comprehension to PA but do not extend the induction scheme to 
the second-order language, we get the conservative extension ACA_0 of PA, 
which proves the T-sentences for first-order sentences.

In order to formally prove that all PA-provable sentences are true we need 
a little bit of induction (Pi^1_1) (see Takeuti's proof theory book). 
Induction is needed in two steps:

1. "All (universal closures of) theorems of PA are true" is proved by 
induction on the length of proofs. The induction clause involves the truth 
predicate.

2. Less obviously, ACA_0 proves only the T-sentences but it does not prove, 
e.g., that a conjunction is true iff both conjuncts are true. ACA_0 proves 
only the corresponding scheme (Proof: Every model of PA can be extended to 
a model of ACA_0, but not every model of PA can be extended to a model of 
PA+"there is a full satisfaction class" (i.e., PA + the Tarski rules)  by a 
theorem due to Lachlan).

So the situation is the same as in set theory where we also don't get the 
Tarski rules in BG, as Ralf said:

>    It should go pretty deep. We can define the truth predicate for set
>theory by a \Sigma^1_1 fmla of class theory and we can prove the Tarski
>schema in BG. However, we (provably) need more than BG in order to prove
>the Tarski rules (for instance, to prove that "if \phi(x) is true for all
>x then \forall v \phi(v) is true");

Ralf, how does one prove that we don't get the Tarski rules in BG?

With best wishes to all
Volker


***************************
Volker Halbach
Universitaet Konstanz
Fachbereich Philosophie
Postfach D21
78457 Konstanz
Germany
Office phone: 07531 88 3524
Fax: 07531 88 4121
Home phone: 07732 970863
http://www.uni-konstanz.de/halbach/index.html
***************************