On the role of implication in formal logic

Journal of Symbolic Logic 65 (3):1076-1114 (2000)
  Copy   BIBTEX


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



    Upload a copy of this work     Papers currently archived: 91,202

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

A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Truth table logic, with a survey of embeddability results.Neil Tennant - 1989 - Notre Dame Journal of Formal Logic 30 (3):459-484.
Paraconsistency and Analyticity.Carlos A. OLLER - 1999 - Logic and Logical Philosophy 7 (1):91-99.
Free Semantics.Ross Thomas Brady - 2010 - Journal of Philosophical Logic 39 (5):511 - 529.
On analysing relevance constructively.Garrel Pottinger - 1979 - Studia Logica 38 (2):171 - 185.
Defining relevant implication in a propositionally quantified S.Philip Kremer - 1997 - Journal of Symbolic Logic 62 (4):1057-1069.


Added to PP

80 (#201,278)

6 months
5 (#526,961)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.
Foundations of Mathematical Logic.William Craig - 1963 - Journal of Symbolic Logic 45 (2):377-378.
Predicate logics without the structure rules.Yuichi Komori - 1986 - Studia Logica 45 (4):393 - 404.
The formulae-as-types notion of construction.William Alvin Howard - 1980 - In Haskell Curry, Hindley B., Seldin J. Roger & P. Jonathan (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press.

View all 7 references / Add more references