Home  Online Resources  Table of Contents

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. jonathan.seldin@uleth.ca

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

  Full-Text PDF  (123 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.