[FOM] Nonconservative law of excluded middle

[Daniel Méhkeri]

You sometimes read that if classical logic proves a
negative then so does intuitionistic logic. This sort
of gives an impression of the conservativity of the
law of the excluded middle (LEM). And as I understand
it this is in fact the case for Heyting (first-order
constructive) arithmetic - it is equiconsistent with
Peano arithmetic.

On the other hand it seems that this is not so for
Aczel's constructive set theory (CZF). CZF is
interpretable in an extension of Martin-Löf
type-theory (augmented with "W-types"), though I don't
claim to understand this interpretation. This is in
turn equiconsistent with a small fragment of
second-order arithmetic. But the axioms of CZF are
such that when LEM is added to it, they become the ZF
axioms (CZF + LEM = ZF), which proves the consistency
of Z, which proves the consistency of umpteenth-order
arithmetic, which proves the consistency of
umpteen-minus-oneth-order arithmetic, which ..., which
proves the consistency of second order arithmetic,
which proves the consistency of any number of systems
down the line, which proves the consistency of CZF.
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.

My zeroth question is, have I got the story right? I
have no formal training in this whatsoever, so reality
checks are appreciated.

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

My second question is can HA be simply extended so
that the translation of PA into HA also fails? 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?

Cheers,
Dan Mehkeri, unaffiliated curious outsider.




      Offrez un compte Flickr Pro à vos amis et à votre famille.
http://www.flickr.com/gift/