Extensional Set Equality in the Calculus of Constructions
Jonathan P. Seldin · Journal of Logic and Computation · 2001
The original representation of set theory in the calculus of constructions, has met an objection on the grounds that the axiom of exstensionality is incompatible with the assumptions for arithmetic. In this paper, it is shown that there is really no problem with the axiom of extensionality. Furthermore, Huet's representation has the advantage that results of Seldin's results imply the consistency of the representation. Having such a consistency proof may be important if one needs a trusted theorem prover, since consistency is clearly a necessary condition (although not a sufficient condition) for being trusted, and the paper closes with some remarks on what makes a system trusted.