[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
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
***************************
More information about the FOM
mailing list