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.
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 ) 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