David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 56 (3):419 - 426 (1996)
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.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
Dag Prawitz (1965/2006). Natural Deduction: A Proof-Theoretical Study. Dover Publications.
J. Lambek & P. J. Scott (1989). Introduction to Higher Order Categorical Logic. Journal of Symbolic Logic 54 (3):1113-1114.
Dag Prawitz & J. E. Fenstad (1975). Ideas and Results in Proof Theory. Journal of Symbolic Logic 40 (2):232-234.
Citations of this work BETA
No citations found.
Similar books and articles
Kevin Morris (2009). Does Functional Reduction Need Bridge Laws? A Response to Marras. British Journal for the Philosophy of Science 60 (3):647-657.
Colin Cheyne (1993). Reduction, Elimination, and Firewalking. Philosophy of Science 60 (2):349-357.
Sachio Hirokawa (1996). The Proofs of Α→Α in P - W. Journal of Symbolic Logic 61 (1):195-211.
Sahotra Sarkar (1992). Models of Reduction and Categories of Reductionism. Synthese 91 (3):167-94.
Michael J. Carroll (1979). Reduction to First Degree in Quantificational S5. Journal of Symbolic Logic 44 (2):207-214.
Wojciech Zielonka (2002). On Reduction Systems Equivalent to the Lambek Calculus with the Empty String. Studia Logica 71 (1):31-46.
E. G. K. López-Escobar (1990). Remarks on the Church-Rosser Property. Journal of Symbolic Logic 55 (1):106-112.
Giorgi Japaridze (2009). Many Concepts and Two Logics of Algorithmic Reduction. Studia Logica 91 (1):1 - 24.
Hongwei Xi (1999). Upper Bounds for Standardizations and an Application. Journal of Symbolic Logic 64 (1):291-303.
Added to index2009-01-28
Total downloads14 ( #179,964 of 1,724,892 )
Recent downloads (6 months)10 ( #64,701 of 1,724,892 )
How can I increase my downloads?