Extension of the definition of the provable totality of a function in the intuitionistic logic HApr.

V. Thibau

IBP-Litp 1995/28: Rapport de Recherche Litp / Litp research reports
36 pages - Juin/June 1995 - Document en anglais.

PostScript : Ko /Kb

Titre / Title: Extension of the definition of the provable totality of a function in the intuitionistic logic HApr.

Résumé : Le but de ce papier est d'étudier complètement la notion de fonction "prouvablement totale" en arithmétique intuitionniste. Le résultat est l'extension de la définition donnée par Kreisel en 1958, d'une fonction prouvablement totale dans une théorie lorsque cette théorie est l'arithmétique intuitionniste. La preuve de ce résultat est intéressante en elle-même puisqu'elle met en évidence les liens profonds qui existent entre l'aritmétique intuitionniste et le système T de Gödel.
Un autre aspect du papier est la comparaison entre l'isomorphisme de Curry-Howard et l'interprétation fonctionnelle introduite par Gödel en 1958 et appelée plus tard Dialectica. "Dialectica fut utilisée par Gödel pour caractériser les fonctions prouvablement totales dans l'arithmétique de Péano au moyen du système T de Gödel.

Abstract : The aim of this paper is to fully study the notion of "provably total function" in the intuitionnistic arithmetic. The obtained result is the extension of the 1958 Kreisel's definition of a "provably total function" in a theory when this theory is the intuitionnistic arithmetic. The proof of this result is interesting by itself since it shows the deep links which exist between the intuitionnistic arithmetic and the functional Gödel's system T.
Another point of the paper is the natural comparison between the Curry-Howard isomorphism and the functional interpretation introduced by Gödel in 1958 (Gödel [13]) and later called Dialectica. "Dialectica" was used by Gödel to characterize the "provably total function" in the Peano's arithmetic by means of the Gödel's system T

Publications internes Litp 1995 / Litp research reports 1995