Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics

摘要

Church's Higher Order Logic is a basis for influential proof assistants --HOL and PVS. Church's logic has a simple set-theoretic semantics, making ittrustworthy and extensible. We factor HOL into a constructive core plus axiomsof excluded middle and choice. We similarly factor standard set theory, ZFC,into a constructive core, IZF, and axioms of excluded middle and choice. Thenwe provide the standard set-theoretic semantics in such a way that theconstructive core of HOL is mapped into IZF. We use the disjunction, numericalexistence and term existence properties of IZF to provide a program extractioncapability from proofs in the constructive core. We can implement the disjunction and numerical existence properties in twodifferent ways: one using Rathjen's realizability for IZF and the other using anew direct weak normalization result for IZF by Moczydlowski. The latter canalso be used for the term existence property.