[FOM] BG and the semantics of set theory
Jeffrey Ketland
ketland at ketland.fsnet.co.uk
Mon Oct 14 17:48:04 EDT 2002
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
~~~~~~~~~~~~~~~~~~~~~~~
More information about the FOM
mailing list