Reduction Rules for Intuitionistic $${{\lambda}{\rho}}$$ λ ρ -calculus

Autor: Ken-etsu Fujita, Yuichi Komori, Naosuke Matsuda, Ryo Kashima
Rok vydání: 2015
Předmět:
Zdroj: Studia Logica. 103:1225-1244
ISSN: 1572-8730
0039-3215
DOI: 10.1007/s11225-015-9616-1
Popis: The third author gave a natural deduction style proof system called the $${{\lambda}{\rho}}$$??-calculus for implicational fragment of classical logic in (Komori, Tsukuba J Math 37:307---320, 2013). In (Matsuda, Intuitionistic fragment of the $${{\lambda}{\mu}}$$?μ-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 $${{\lambda}{\rho}}$$??-calculus" of the $${{\lambda}{\rho}}$$??-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus (Kripke models), but is complicated. In this paper, we introduce some reduction rules for the $${{\lambda}{\rho}}$$??-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.
Databáze: OpenAIRE
Externí odkaz: