# Collections, Sets and Types

Abstract : We give a first order formulation of Church's type theory in which types are mere sets. This formulation is obtained by replacing $\lambda$-calculus by a language of combinators (skolemized comprehension scheme), introducing a distinction between propositions and their contents, relativizing quantifiers and at last replacing typing predicates by membership to some sets. The theory obtained this way has both a type theoretical flavor and a set theoretical one. Like set theory, it is a first order theory, and it uses only one notion of collection. Like type theory, it gives an explicit notation for objects, a primitive notion of function and propositions are objects.
Keywords :
Type de document :
Rapport
[Research Report] RR-2708, INRIA. 1995
Domaine :

https://hal.inria.fr/inria-00073982
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:13:58
Dernière modification le : samedi 17 septembre 2016 - 01:27:45
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:03:14

### Identifiants

• HAL Id : inria-00073982, version 1

### Citation

Gilles Dowek. Collections, Sets and Types. [Research Report] RR-2708, INRIA. 1995. 〈inria-00073982〉

### Métriques

Consultations de la notice

## 128

Téléchargements de fichiers