A Type-Free Formalization of Mathematics where Proofs are Objects

Abstract : We present a first order untyped axiomatization of mathematics where proofs are objects in the sense of Heyting-Kolmogorov functional interpretation. The consistency of this theory is open.
Type de document :
Rapport
[Research Report] RR-2915, INRIA. 1996
Liste complète des métadonnées

https://hal.inria.fr/inria-00073782
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:44:55
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:58:03

Fichiers

Identifiants

  • HAL Id : inria-00073782, version 1

Collections

Citation

Gilles Dowek. A Type-Free Formalization of Mathematics where Proofs are Objects. [Research Report] RR-2915, INRIA. 1996. 〈inria-00073782〉

Partager

Métriques

Consultations de la notice

72

Téléchargements de fichiers

107