|
Zapiski Nauchnykh Seminarov LOMI, 1974, Volume 40, Pages 110–118
(Mi znsl2686)
|
|
|
|
On $E$-theorems
G. E. Mints
Abstract:
There are [1] many methods to construct for every proof of a sentence $\exists x A$ in Heyting (intuitionistic) arithmetic $HA$ [2] a term $t_p$ such that $A[t_p]$ is true (in some sence). It turns out that majority of these methods are equivalent: correspondent terms $t_p$ are convertible into one and the same natural number. This is proved here for three methods: (I) complete cut-elimination in the infinite formulation of $HA$ [3]; (II) recursive realizability [2]; (III) partial cut-elimination along the lines of Gentsen's 2-nd consistency proof [5]. [6] or normalization [7], [8]. It is shown that the process of cut-elimination by method (I) leads only to computation of values of terms associated with a given proof by methods (II) and (III).
Citation:
G. E. Mints, “On $E$-theorems”, Studies in constructive mathematics and mathematical logic. Part VI, Zap. Nauchn. Sem. LOMI, 40, "Nauka", Leningrad. Otdel., Leningrad, 1974, 110–118
Linking options:
https://www.mathnet.ru/eng/znsl2686 https://www.mathnet.ru/eng/znsl/v40/p110
|
Statistics & downloads: |
Abstract page: | 136 | Full-text PDF : | 46 |
|