[FOM] FOM: The semantics of set theory

Volker Halbach Volker.Halbach at uni-konstanz.de
Wed Oct 9 14:19:48 EDT 2002

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 

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 Halbach
Universitaet Konstanz
Fachbereich Philosophie
Postfach D21
78457 Konstanz
Office phone: 07531 88 3524
Fax: 07531 88 4121
Home phone: 07732 970863

More information about the FOM mailing list