A reduction rule for Peirce formula

Studia Logica 56 (3):419 - 426 (1996)
  Copy   BIBTEX


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.



    Upload a copy of this work     Papers currently archived: 92,907

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Does functional reduction need bridge laws? A response to Marras.Kevin Morris - 2009 - British Journal for the Philosophy of Science 60 (3):647-657.
Remarks on the church-Rosser property.E. G. K. López-Escobar - 1990 - Journal of Symbolic Logic 55 (1):106-112.
Reduction to first degree in quantificational S5.Michael J. Carroll - 1979 - Journal of Symbolic Logic 44 (2):207-214.
The proofs of α→α in P - W.Sachio Hirokawa - 1996 - Journal of Symbolic Logic 61 (1):195-211.
Entanglement, joint measurement, and state reduction.Alan Macdonald - 2003 - International Journal of Theoretical Physics 42:943-953.
Reduction, elimination, and firewalking.Colin Cheyne - 1993 - Philosophy of Science 60 (2):349-357.


Added to PP

66 (#251,409)

6 months
11 (#270,425)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1971 - Journal of Symbolic Logic 40 (2):232-234.
Introduction to Higher Order Categorical Logic.J. Lambek & P. J. Scott - 1989 - Journal of Symbolic Logic 54 (3):1113-1114.
Introduction to Combinators and (Lambda) Calculus.J. Roger Hindley - 1986 - New York: Cambridge University Press. Edited by J. P. Seldin.

Add more references