Abstract
We review here some intuitionistic systems with choice principles
for which normalization theorems have been established. These are mainly first order systems or systems close to the first order ones in their deductive power. This is not accidental, since in higher order intuitionistic logic with extensionality choice seems to imply excluded third [1].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
N. Goodman and J. Myhill, Choice implies excluded middle, Z.math.Log. and Grundl.Math. 24: 461 (1978).
G. E. Mints, Heyting predicate calculus with epsilon—symbol, Zap. Nauch.Sem. Leningrad.Otd.Mat.Inst. Akad. Nauk SSSR 40:101 (1974). English translation: J.Sovïath. 8: 317 (1977).
A. Dragalin, Intuitionistic logic and Hilbert’s epsilon—symbol, in: “History and Methodology of Natural Sciences,” Moscow Univ. Press, Moscow 16:78 (1974) (in Russian).
D. Leivant, “Existential Instantiation in a System of Natural Deduction for Intuitionistic Arithmetic,” Stichting Math. Centrum, Amsterdam (1973).
S. Maehara, A general theory of completeness proofs, Ann.Jap. Ass. Philos.Sci. 3:54 (1970).
K. Shirai, Intuitionistic predicate calculus with epsilon—symbols, Ann.Jap.Ass.Philos.Sci. 4: 49 (1971).
V. Smirnov, Elimination des termes epsylon dans le logique intuitioniste, Revue Intern, de Philosophie 98: 512 (1971).
G. Mints, Skolem’s method of elimination of positive quantifiers in sequential calculi, Soviet Math. Dokl. 7:861 (1966).
C. Smorynski, On axiomatizing fragments, J.Symbol.Log. 42: 530 (1977).
D. Miller and G. Nadatur, Higher order logic programming, in: “Proc. Third Int. Logic Progr. Conf.,” London, June 1986, 448.
G. Mints, The Herbrand theorem, in: “Mathematical Theory of Logical Deduction,” Nauka, Moscow (1967), 311 (in Russian).
G. Mints, Finite investigation of infinite derivations, Zap.Nauch.Sem. Leningrad.Otd.Mat.Inst. Akad. Nauk SSSR 49:57 (1975). English translation: J.Sov.Math. 10: 548 (1978).
H. Schwichtenberg, A normal form for natural deduction in a type theory with realizing terms, in: Atti del Congresso, “Logica e Filosofia della Scienza,” Logica. CLUEB, Bologna (1986), I: 95.
A. Leisenring, “Mathematical Logic and Hilbert’s Epsilon—symbol,” MacDonald, London (1969).
H. Osswald, Über Skolemerweiterungen in der intuitionistischen Logik mit Gleichheit, Lect. Notes Math. 500:264 (1975).
N. Goodman, The faithfulness of the interpretation of arithmetic in the theory of constructions, J. Symbolic Logic 38:453 (1973).
P. Howard, The formulae—as—types notation of construction, in: “To H. B. Curry. Essays on Logic, Lambda Calculus and Formalism,” Academic Press, London (1980), 479–490.
A. Troelstra, ed., Mathematical investigation of intuitionistic arithmetic and analysis, Lect. Notes Math. N344 (1973).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Plenum Press, New York
About this chapter
Cite this chapter
Mints, G. (1990). Normalization Theorems for the Intuitionistic Systems with Choice Principles. In: Petkov, P.P. (eds) Mathematical Logic. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-0609-2_6
Download citation
DOI: https://doi.org/10.1007/978-1-4613-0609-2_6
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4612-7890-0
Online ISBN: 978-1-4613-0609-2
eBook Packages: Springer Book Archive