Extraction in IZF
by Wojciech Moczydlowski
2004-2005
IZF is an intuitionistic version of Zermelo-Fraenkel set theory (ZFC). We present a practical approach to doing extraction in IZF, based on formulas-as-types principle.
IZF is an intuitionistic version of Zermelo-Fraenkel set theory (ZFC). We present a practical approach to doing extraction in IZF, based on formulas-as-types principle.