[FOM] FOM Digest, Vol 65, Issue 4, Nonconservative law of excluded middle (Daniel M?hkeri)

[rathjen@maths.leeds.ac.uk]

>Whew! This is a pretty spectacular non-conservativity!

>I also read that this can be extended to large
>cardinal axioms, in that there are certain "large set"
>axioms LSA such that CZF+LSA is still provably
>consistent in second order arithmetic, but CZF+LSA+LEM
>is equiconsistent (or identical?) with a corresponding
>large cardinal axiom. I only have a very vague idea
>what a large set axiom is about.

Yes, this has been explored for some large set existence axioms (LSA )
such as
axioms asserting the existence of inaccessible, Mahlo, and weakly compact
sets.  In these cases CZF+LSA  can be proven to be consistent in a
fragment of second order arithmetic (e.g. Pi^1_2 comprehension)

>My zeroth question is, have I got the story right?

Yes,  that's the case.

>My first question is how far is the "large set" thing
>known to go?

See above. Up to weakly compact this has been investigated.
 To my knowledge this has not been explored for CZF augmented by very
large LSA such as measurable, supercompact, huge etc.

>E.g. is
>there a well-founded relation such that HA +
>transfinite induction along that relation is provably
>consistent in the same system plus LEM, as with CZF?
>If so, are there such well-founded relations which are
>natural?

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


Michael Rathjen
Professor of Mathematics
University of Leeds