[FOM] BG and the semantics of set theory

[Ralf Schindler]

Dear FOMers,
   my last posting contained a misquotation. The two versions of BG 
I had discussed are really the same, although I had intended to discuss 
versions which are different from each other. Namely, as the weaker 
version of BG I had in mind one in which the instances of the 
comprehension schema are \Sigma^1_1 rather than \Pi^1_2 statements of 
class theory. 
   Anyway, here's a final summary of what holds true.

   In the languange of BG, the truth predicate T(v) is defined as 
\exists X \exists n (t(X,n) and  v \in X); here, t(X,n) says that X
contains exactly the set theoretical truths of rank < n. t(X,n) is 
\Sigma^1_0, so T(v) is \Sigma^1_1.
   Lemma 1. GB proves the Tarski schema.
   Proof. Easy. -|
   Lemma 2. BG does not prove the Tarski rules.
   Proof. Let (M;E) be a model of ZF which has non-standard integers.
Let K be the set of all subsets of M which are definable over (M;E) 
(with parameters from M). Then (M,K;E) is a model of BG. However, only 
standard Godel numbers e can satisfy (M,K;E) \models T(e). Therefore,
the Tarski rule for negation is wrong in (M,K;E). -|
   Lemma 3. BG + \Sigma^1_1 induction does prove the Tarski rules.
   Proof. BG proves the statement that for each n there is at most one
X with t(X,n). BG + \Sigma^1_1 induction for the integers can be used 
to prove that for each n there is an X with t(X,n). -|
   
   The fact that we do not have to presuppose the existence of 
non-predicateive classes when defining the truth predicate for set 
theory should be philosophically interesting. Hence my question to 
you, the FOM community: where do the above (easy) results show up in 
the literature?
   Thanks, Ralf

-- 
---------------------------------------------------------------------
Ralf Schindler                                Phone: +43-1-4277-50511
Institut fuer Formale Logik                     Fax: +43-1-4277-50599
Universitaet Wien                      E-mail: rds at logic.univie.ac.at
1090 Wien, Austria           URL: http://www.logic.univie.ac.at/~rds/
---------------------------------------------------------------------