[FOM] Nonconservative law of excluded middle
Andrej.Bauer at andrej.com
Mon May 5 18:21:41 EDT 2008
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
More information about the FOM