The theory of the Gödel functionals
- 1 September 1976
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 41 (3), 574-582
- https://doi.org/10.2307/2272035
Abstract
In [2] we described an arithmetic theory of constructions (ATC) and showed that first-order intuitionistic arithmetic (HA) could be interpreted in it. In [3] we went on to show that the interpretation of HA in ATC is faithful. The purpose of the present paper is to apply these ideas to intuitionistic arithmetic in all finite types. Tait has shown [6] that a conservative extension of HA is obtained by adding the Gödel functionals with intuitionistic logic and intensional identity in all finite types. Below we show that this extension remains conservative on the addition of certain axioms of choice which are evident on the intended interpretation of the intuitionistic logical connectives. This theorem (Corollary 6.2 below) was first obtained by a more complicated argument in our dissertation [1]. Some of its implications are discussed in Goodman and Myhill [4].We assume that the reader is familiar with [2] and [3].Keywords
This publication has 1 reference indexed in Scilit:
- The formalization of Bishop's constructive mathematicsPublished by Springer Science and Business Media LLC ,1972