Graduate studies at Western
Studia Logica 56 (3):419 - 426 (1996)
|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.|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
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 downloads4 ( #189,469 of 740,510 )
Recent downloads (6 months)1 ( #61,957 of 740,510 )
How can I increase my downloads?