[FOM] RE : Nonconservative law of excluded middle
Daniel Méhkeri
dmehkeri at yahoo.ca
Wed May 7 21:27:44 EDT 2008
Thank you Dr. Rathjen for your answers.
I have a question about your example:
> The proof-theoretic ordinal of CZF is the so-called
> Bachmann-Howard ordinal which is a (well-known to
> proof theorists) natural well-founded relation <.
> CZF proves the same Pi^0_2 statements as PA +
> transfinite induction for all (meta) initial
> segments of <. The latter theory proves the same
> Pi^0_2 statements as HA + transfinite induction
> for all (meta) initial segments of <.
But then PA + transfinite induction along it could not
prove consistency of HA + transfinite induction along
it, could it? I expect I have misunderstood your
example, or else my original question was badly
worded: I was really wondering about HA + X + LEM
proving Con(HA + X).
As to the even larger set axioms you mentioned
(measurable, supercompact, huge etc) may I also ask
what you think the range of plausible strengths would
be for such extensions? I ask because someone else
gave a URL to the paper of yours with the suggestive
title "Inaccessible Set Axioms May Have Little
Consistency Strength". Do you expect them all to be
below, say, second-order arithmetic?
I also notice that paper uses something weaker than
CZF (namely it drops well-foundation), and with a
large set axiom it only goes up to the
Feferman-Schütte ordinal, but with LEM, it goes to the
existence of strong inaccessibles. This for me is even
more striking because though the Feferman-Schütte
ordinal is over my head, I think I can write a
fundamental sequence for it, and sequences for
elements of that sequence, and on down to zero, even
without having any clear sense of what it _is_. As for
the Bachmann-Howard ordinal, at the moment I can
pronounce "Bachmann-Howard". But that's about it.
Regards,
Dan
Offrez un compte Flickr Pro à vos amis et à votre famille.
http://www.flickr.com/gift/
More information about the FOM
mailing list