Rapport de Recherche Litp /
Litp research reports
26 pages - Juin/June 1995 - Document en anglais.
PostScript : Ko /Kb
Titre / Title: A refinement of a part of Gödel's theorem on provably total functions of PA.
Abstract : The aim of this paper is to give the detailed proof of the fact that any closed term of T of type iÆi represents a provably total function of PA (or HA) from N to N and to get a refinement of this Gödel's theorem's part with a careful coding of the Gödel's system T in the Peano's arithmetics. All the notions used here are defined in a previous report: Extension of the definition of the provable totality of a function in the intuitionistic logic HApr.
Publications internes Litp 1995 / Litp research reports 1995