[FOM] BG and the semantics of set theory

[Ralf Schindler]

On Mon, 14 Oct 2002, Jeffrey Ketland wrote:

> And, since T(v) is itself \Sigma^1_1, do we have:
> Corollary: BG + \Sigma^1_1 induction proves Global Reflection Principle for
> ZF?
> 
> I.e., BG + \Sigma^1_1 induction proves the statement "forall x \in
> LST(Bew_ZF(x) -> T(x))"?

   Yes. Work in BG + \Sigma^1_1 ind. First prove that every axiom of ZF
is true. To do this for the separation and replacement schema one uses
induction on the complexity of the relevant formula. (To make this work, 
use an appropriate formulation of replacement.) Then prove that every 
proof in ZF only yields truths. This is done by an induction on the length
of proofs. Both steps use the Tarski rules.
   Thank you for pointing out that this should hold true! --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/
---------------------------------------------------------------------