[FOM] RE : Nonconservative law of excluded middle

[Daniel Méhkeri]

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/