A refinement of a part of Gödel's theorem on provably total functions of PA.

V. Thibau.

IBP-Litp 1995/29: 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.

Résumé : e but de ce papier est de donner la preuve détaillée du fait que tout terme clos du système T de type iÆi represente une fonction prouvablement totale de PA (ou HA) de N vers N et d'obtenir un raffinement de cette partie du théorème de Gödel moyennant un codage soigneux du système T de Gödel dans l'arithmétique de Peano. Toutes les notions utilisées sont définies dans un rapport précédent: Extension of the definition of the provable totality of a function in the intuitionistic logic HApr.

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