Abstract
A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a λ-calculus with a new constant P ((α→β)→α). It is shown that all terms with the same type are equivalent with respect to β-reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for βP-reduction. Weak normalization is shown for βP-reduction with another reduction rule which simplifies α of ((α → β) → α) → α into an atomic type.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Hindley, J. R. and J. P. Seldin, 1986, Introduction to Combinators and Lambda-Calculus, Cambridge University Press, London.
Hirokawa, S., Y. Komori and I. Takeuti, 1995, A reduction rule for the Peirce formula (abstract), Bulletin of Symbolic Logic, 1, 239–240.
Lambek, J. and P. J. Scott, 1986, Introduction to higher order categorical logic, Cambridge University Press, London.
Prawitz, D., 1965, Natural Deduction, Almqvist and Wiksell, Stockholm.
Prawitz, D., 1971, Ideas and results in proof theory. In Proc. 2nd Scandinavian Logic Symposium, ed. J.E. Fenstad. North-Holland, 235–307.
Author information
Authors and Affiliations
Additional information
This work was partially supported by a Grant-in-Aid for General Scientific Research No. 05680276 of the Ministry of Education, Science and Culture, Japan and by Japan Society for the Promotion of Science.
Rights and permissions
About this article
Cite this article
Hirokawa, S., Komori, Y. & Takeuti, I. A reduction rule for Peirce formula. Stud Logica 56, 419–426 (1996). https://doi.org/10.1007/BF00372774
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF00372774