[FOM] FOM: The semantics of set theory
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
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
Office phone: 07531 88 3524
Fax: 07531 88 4121
Home phone: 07732 970863
More information about the FOM