- New
-
Topics
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- Journals
- Submit material
- More
Some properties of the -calculus
Journal of Applied Non-Classical Logics 22 (3):231-247 (2012)
Abstract
In this paper, we present the -calculus which at the typed level corresponds to the full classical propositional natural deduction system. The Church–Rosser property of this system is proved using the standardisation and the finiteness developments theorem. We also define the leftmost reduction and prove that it is a winning strategy.Other Versions
No versions found
My notes
Similar books and articles
Church–Rosser property of a simple reduction for full first-order classical natural deduction.Y. Andou - 2003 - Annals of Pure and Applied Logic 119 (1-3):225-237.
Strong normalization results by translation.René David & Karim Nour - 2010 - Annals of Pure and Applied Logic 161 (9):1171-1179.
Church-Rosser property and intersection types.George Koletsos & George Stavrinos - 2008 - Australasian Journal of Logic 6:37-54.
Natural deduction systems for Nelson's paraconsistent logic and its neighbors.Norihiro Kamide - 2005 - Journal of Applied Non-Classical Logics 15 (4):405-435.
Propositional Mixed Logic: Its Syntax and Semantics.Karim Nour & Abir Nour - 2003 - Journal of Applied Non-Classical Logics 13 (3-4):377-390.
A proof-theoretic investigation of a logic of positions.Stefano Baratella & Andrea Masini - 2003 - Annals of Pure and Applied Logic 123 (1-3):135-162.
Reduction Rules for Intuitionistic $${{\lambda}{\rho}}$$ λ ρ -calculus.Ken-Etsu Fujita, Ryo Kashima, Yuichi Komori & Naosuke Matsuda - 2015 - Studia Logica 103 (6):1225-1244.
Opérateurs de mise en mémoire et traduction de Gödel.Jean-Louis Krivine - 1990 - Archive for Mathematical Logic 30 (4):241-267.
Logics of rejection: two systems of natural deduction.Allard Tamminga - 1994 - Logique Et Analyse 146:169-208.
The modalized Heyting calculus: a conservative modal extension of the Intuitionistic Logic ★.Leo Esakia - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):349-366.
Analytics
Added to PP
2013-10-30
Downloads
31 (#732,022)
6 months
5 (#1,053,842)
2013-10-30
Downloads
31 (#732,022)
6 months
5 (#1,053,842)
Historical graph of downloads
References found in this work
The lambda calculus: its syntax and semantics.Hendrik Pieter Barendregt - 1984 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Church–Rosser property of a simple reduction for full first-order classical natural deduction.Y. Andou - 2003 - Annals of Pure and Applied Logic 119 (1-3):225-237.
Non-strictly positive fixed points for classical natural deduction.Ralph Matthes - 2005 - Annals of Pure and Applied Logic 133 (1):205-230.
A short proof of the strong normalization of classical natural deduction with disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
Recherches sur la Déduction Logique.Gerhard Gentzen & Robert Feys - 1957 - Journal of Symbolic Logic 22 (4):350-351.
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-648784bb4d-xlp8h uwo