[FOM] Nonconservative law of excluded middle

[Andrej Bauer]

hendrik at topoi.pooq.com wrote:
> On Thu, May 01, 2008 at 09:51:22PM -0400, Daniel Méhkeri wrote:
>> 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 I didn't know.  Could you provide a reference?
> (preferably on-line; I don't have easy access to a library)

A recent reference is:

"The Generalised Type-theoretic Interpretation of Constructive Set
Theory", by Nicola Gambino and Peter Aczel, in the Journal of Symbolic
Logic, Volume 71, Number 1, March (2006), 67-103.

Available at: http://www.cs.man.ac.uk/~petera/gambino-aczel.ps.gz

A more original reference is, I think:

"The Type Theoretic Interpretation of Constructive Set Theory" by Peter
Aczel. In Angus Macintyre; Leszek Pacholski; Jeff Paris, editors.
Logic colloqium '77, pages 55-66. North-Holland, 1978.

>> Whew! This is a pretty spectacular non-conservativity!
> 
> Spectacular enough that I'd like to see the details here, too.

"Inaccessible Set Axioms May Have Little Consistency Strength"
by L. Crosilla, M. Rathjen

Available at: http://citeseer.ist.psu.edu/384300.html

You want Lemma 2.7.

(You have to use the cached version because the original link does not
work anymore.)

Best regards,

Andrej