Abstract
The usual rule used to obtain natural deduction formulations of classical logic from intuitionistic logic, namely
is stronger then necessary, and will give classical logic when added to minimal logic. A rule which is precisely strong enough to give classical logic from intuitionistic logic, and which is thus exactly equivalent to the law of the excluded middle, is
It is a special case of a version of Peirce's law:
In this paper it is shown how to normalize logics defined using these last two rules. Part I deals with propositional logics and first order predicate logics. Part II will deal with first order arithmetic and second order logics.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
H. B. Curry,A Theory of Formal Deducibility, Notre Dame Mathematical Lectures No. 6, Notre Dame, Indiana, 1950. Second Edition 1957.
H. B. Curry,The system LD,Journal of Symbolic Logic 17 (1952), pp. 35–42.
H. B. Curry,Foundations of Mathematical Logic, McGraw-Hill, New York, 1963. Reprinted by Dover, 1977 and 1984.
H. B. Curry,A deduction theorem for inferential predicate calculus, inContributions to Mathematical Logic (ed. K. Schütte), North-Holland, Amsterdam, 1968, pp. 91–108.
M. V. Glivenko,Sur quelques points de la logique de M. Brouwer,Acad. Roy. Belg. Bull. Cl. Sci. 15 (1929), pp. 183–188.
N. Muti,On application of Peirce's rule: a solution of Curry's problem, unpublished typescript, 1967.
D. Prawitz,Natural Deduction: a Proof Theoretical Study, Almqvist & Wiksell, Stockholm, 1965.
D. Prawitz,Ideas and results in proof theory, inProceedings of the Second Scandinavian Logic Symposium (ed. J. E. Fenstad), North-Holland, Amsterdam, 1971, pp 235–307.
J. P. Seldin,Proof normalizations and generalizations of Glivenko's theorem (abstract), volume of contributed papers for the Fifth International Congress of Logic, Methodology and Philosophy of Science, London, Ontario, August–September 1975, pp. I 43–44.
J. P. Seldin,Normalization for second order logics with excluded middle (abstract),Journal of Symbolic Logic 46 (1981), pp. 430–431.
J. P. Seldin,On the proof theory of the intermediate logic MH,Journal of Symbolic Logic 51 (1986), pp. 626–647.
W. W. Tait,Intensional interpretations of functionals of finite type,Journal of Symbolic Logic 32 (1967), pp. 198–212.
Author information
Authors and Affiliations
Additional information
This research was supported in part by grants EQ1648, EQ2908, and CE 110 of the program Fonds pour la Formation de Chercheurs et l'aide à la Recherche (F.C.A.R.) of the Quèbec Ministry of Education.
Rights and permissions
About this article
Cite this article
Seldin, J.P. Normalization and excluded middle. I. Stud Logica 48, 193–217 (1989). https://doi.org/10.1007/BF02770512
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02770512