[FOM] BG and the semantics of set theory

[Jeffrey Ketland]

Ralf Schindler wrote:

>   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). -|

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))"?

>   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?

Yes, it is philosophically interesting and I wish I knew more about this.
There are various bits of scattered literature pointing out that truth
axioms are related to predicative set/class comprehension. (E.g., the close
relation of Feferman's Tr(PA) and ACA).

--- Jeff

~~~~~~~~~~~~~~~~~~~~~~~
Jeffrey Ketland
School of Philosophy
University of Leeds
LEEDS LS2 9JT
U.K.
ketland at ketland.fsnet.co.uk
~~~~~~~~~~~~~~~~~~~~~~~