Journal of Logic and Computation, Volume 11, Issue 3, pp. 483-493: Abstract.
Extensional Set Equality in the Calculus of Constructions
Jonathan P. Seldin
Department of Mathematics and Computer Science, University of Lethbridge, Lethbridge, Alberta, Canada. email@example.com
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.
Keywords: Extensionality, typed [lambda], -, calculus, calculus of constructions, set theory, trusted systems