- Report number: 1995-052
- Authors: V. THIBAU
- Title: A refinement of a part of gödel's theorem on provably total functions of PA.
The aim of this paper is to give the detailed proof of the fact that any closed terrez of T of type iAEi represents a provably total function of PA (or HA) from N to N and to get a refinement of this Gödel's theorems part with a careful coding of the Gödel's system T in the Peanos 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.