On the role of implication in formal logic
Journal of Symbolic Logic 65 (3):1076-1114 (2000)
| Abstract | Evidence is given that implication (and its special case, negation) carry the logical strength of a system of formal logic. This is done by proving normalization and cut elimination for a system based on combinatory logic or λ-calculus with logical constants for and, or, all, and exists, but with none for either implication or negation. The proof is strictly finitary, showing that this system is very weak. The results can be extended to a "classical" version of the system. They can also be extended to a system with a restricted set of rules for implication: the result is a system of intuitionistic higher-order BCK logic with unrestricted comprehension and without restriction on the rules for disjunction elimination and existential elimination. The result does not extend to the classical version of the BCK logic | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,679 |
| External links |
|
| Through your library | Configure |
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Philip Kremer (1997). Defining Relevant Implication in a Propositionally Quantified S. Journal of Symbolic Logic 62 (4):1057-1069.
Garrel Pottinger (1979). On Analysing Relevance Constructively. Studia Logica 38 (2):171 - 185.
Ross Thomas Brady (forthcoming). Free Semantics. Journal of Philosophical Logic.
Carlos A. OLLER (1999). Paraconsistency and Analyticity. Logic and Logical Philosophy 7 (1):91-99.
Peter Milne (1994). Classical Harmony: Rules of Inference and the Meaning of the Logical Constants. Synthese 100 (1):49 - 94.
Arnold Koslow (1992/2005). A Structuralist Theory of Logic. Cambridge University Press.
Neil Tennant (1989). Truth Table Logic, with a Survey of Embeddability Results. Notre Dame Journal of Formal Logic 30 (3):459-484.
Mitsuhiro Okada (1987). A Weak Intuitionistic Propositional Logic with Purely Constructive Implication. Studia Logica 46 (4):371 - 382.
Ryo Kashima & Norihiro Kamide (1999). Substructural Implicational Logics Including the Relevant Logic E. Studia Logica 63 (2):181-212.
Monthly downloads |
Added to index2009-01-28Total downloads6 ( #145,615 of 549,071 )Recent downloads (6 months)1 ( #63,317 of 549,071 )How can I increase my downloads? |

