Studia Logica 103 (6):1225-1244 (2015)

The third author gave a natural deduction style proof system called the \-calculus for implicational fragment of classical logic in. In -calculus, 2015, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear), the fourth author gave a natural subsystem “intuitionistic \-calculus” of the \-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus, but is complicated. In this paper, we introduce some reduction rules for the \-calculus, and give a simple and purely syntactical proof to the theorem by use of the reduction. In addition, we show that we can give a computation model with rich expressive power with our system
Keywords $${{\lambda}{\rho}}$$ λ ρ -calculus  Curry–Howard isomorphism  Intuitionistic logic  Proof theory
Categories (categorize this paper)
DOI 10.1007/s11225-015-9616-1
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 59,775
External links

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

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Light Affine Lambda Calculus and Polynomial Time Strong Normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
A Lambda Proof of the P-W Theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
Atomic Polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
Weak Typed Böhm Theorem on IMLL.Satoshi Matsuoka - 2007 - Annals of Pure and Applied Logic 145 (1):37-90.
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.


Added to PP index

Total views
32 ( #330,510 of 2,432,669 )

Recent downloads (6 months)
2 ( #294,596 of 2,432,669 )

How can I increase my downloads?


My notes