[FOM] Nonconservative law of excluded middle
hendrik at topoi.pooq.com
Sat May 3 15:34:48 EDT 2008
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)
> Whew! This is a pretty spectacular non-conservativity!
Spectacular enough that I'd like to see the details here, too.
More information about the FOM