10 found
Sort by:
  1. Yuichi Komori, Naosuke Matsuda & Fumika Yamakawa (2014). A Simplified Proof of the Church–Rosser Theorem. 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)  
     
    My bibliography  
     
    Export citation  
  2. Yuichi Komori & Arato Cho (2002). 1 The Type Free Λρ-Calculus. Bulletin of the Section of Logic 31 (2):65-70.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  3. Sachio Hirokawa, Yuichi Komori & Misao Nagayama (2000). A Lambda Proof of the P-W Theorem. Journal of Symbolic Logic 65 (4):1841-1849.
    The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes B = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α = β holds if α → β and β → α are both provable in P-W. The answer is (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  4. Sachio Hirokawa, Yuichi Komori & Izumi Takeuti (1996). A Reduction Rule for Peirce Formula. Studia Logica 56 (3):419 - 426.
    A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a -calculus with a new constant P (()). It is shown that all terms with the same type are equivalent with respect to -reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for P-reduction. Weak normalization is shown for P-reduction with another (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  5. Yuichi Komori (1994). Syntactical Investigations intoBI Logic andBB′I Logic. Studia Logica 53 (3):397 - 416.
    In this note, we will study four implicational logicsB, BI, BB and BBI. In [5], Martin and Meyer proved that a formula is provable inBB if and only if is provable inBBI and is not of the form of » . Though it gave a positive solution to theP - W problem, their method was semantical and not easy to grasp. We shall give a syntactical proof of the syntactical relation betweenBB andBBI logics. It also includes a syntactical proof of (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  6. Yuichi Komori & Sachio Hirokawa (1993). The Number of Proofs for a BCK-Formula. Journal of Symbolic Logic 58 (2):626-628.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  7. Yuichi Komori (1989). Logic Based on Combinators. Bulletin of the Section of Logic 18 (3):100-104.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  8. Yuichi Komori (1986). A New Semantics for Intuitionistic Predicate Logic. Studia Logica 45 (1):9 - 17.
    The main part of the proof of Kripke's completeness theorem for intuitionistic logic is Henkin's construction. We introduce a new Kripke-type semantics with semilattice structures for intuitionistic logic. The completeness theorem for this semantics can he proved without Henkin's construction.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  9. Yuichi Komori (1986). Predicate Logics Without the Structure Rules. Studia Logica 45 (4):393 - 404.
    In our previous paper [5], we have studied Kripke-type semantics for propositional logics without the contraction rule. In this paper, we will extend our argument to predicate logics without the structure rules. Similarly to the propositional case, we can not carry out Henkin's construction in the predicate case. Besides, there exists a difficulty that the rules of inference () and () are not always valid in our semantics. So, we have to introduce a notion of normal models.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  10. Hiroakira Ono & Yuichi Komori (1985). Logics Without the Contraction Rule. Journal of Symbolic Logic 50 (1):169-201.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation