7 found
Order:
  1.  32
    Effect of the Choice of Connectives on the Relation between Classical Logic and Intuitionistic Logic.Tomoaki Kawano, Naosuke Matsuda & Kento Takagi - 2022 - Notre Dame Journal of Formal Logic 63 (2).
  2.  43
    On Implicational Intermediate Logics Axiomatizable by Formulas Minimal in Classical Logic: A Counter-Example to the Komori–Kashima Problem.Yoshiki Nakamura & Naosuke Matsuda - 2021 - Studia Logica 109 (6):1413-1422.
    The Komori–Kashima problem, that asks whether the implicational intermediate logics axiomatizable by formulas minimal in classical logic are only intuitionistic logic and classical logic, has stood for over a decade. In this paper, we give a counter-example to this problem. Additionally, we also give some open problems derived from this result.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  44
    A Simplified Proof of the Church–Rosser Theorem.Yuichi Komori, Naosuke Matsuda & Fumika Yamakawa - 2014 - Studia Logica 102 (1):175-183.
    Takahashi translation * is a translation which means reducing all of the redexes in a λ-term simultaneously. In [4] and [5], Takahashi gave a simple proof of the Church–Rosser confluence theorem by using the notion of parallel reduction and Takahashi translation. Our aim of this paper is to give a simpler proof of Church–Rosser theorem using only the notion of Takahashi translation.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  4.  14
    Definability of Boolean Functions in Kripke Semantics.Naosuke Matsuda - 2023 - Notre Dame Journal of Formal Logic 64 (3):363-376.
    A set F of Boolean functions is said to be functionally complete if every Boolean function is definable by combining functions in F. Post clarified when a set of Boolean functions is functionally complete (with respect to classical semantics). In this paper, by extending Post’s theorem, we clarify when a set of Boolean functions is functionally complete with respect to Kripke semantics.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  5.  36
    Reduction Rules for Intuitionistic $${{\lambda}{\rho}}$$ λ ρ -calculus.Ken-Etsu Fujita, Ryo Kashima, Yuichi Komori & Naosuke Matsuda - 2015 - Studia Logica 103 (6):1225-1244.
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  6.  20
    Term-Space Semantics of Typed Lambda Calculus.Ryo Kashima, Naosuke Matsuda & Takao Yuyama - 2020 - Notre Dame Journal of Formal Logic 61 (4):591-600.
    Barendregt gave a sound semantics of the simple type assignment system λ → by generalizing Tait’s proof of the strong normalization theorem. In this paper, we aim to extend the semantics so that the completeness theorem holds.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  7.  10
    Cut-free sequent calculi for logics characterized by finite linear Kripke frames.Naosuke Matsuda - 2017 - Logic Journal of the IGPL 25 (5):686-696.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark