11 found
Order:
  1.  28
    Logics Without the Contraction Rule.Hiroakira Ono & Yuichi Komori - 1985 - Journal of Symbolic Logic 50 (1):169-201.
  2.  30
    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  
  3.  14
    Predicate Logics Without the Structure Rules.Yuichi Komori - 1986 - 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)  
     
    Export citation  
     
    Bookmark   12 citations  
  4.  23
    Syntactical Investigations intoBI Logic andBB′I Logic.Yuichi Komori - 1994 - 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)  
     
    Export citation  
     
    Bookmark   2 citations  
  5.  34
    A Reduction Rule for Peirce Formula.Sachio Hirokawa, Yuichi Komori & Izumi Takeuti - 1996 - 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)  
     
    Export citation  
     
    Bookmark   1 citation  
  6.  25
    A New Semantics for Intuitionistic Predicate Logic.Yuichi Komori - 1986 - 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)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  15
    The Number of Proofs for a BCK-Formula.Yuichi Komori & Sachio Hirokawa - 1993 - Journal of Symbolic Logic 58 (2):626-628.
  8.  24
    A Lambda Proof of the P-W Theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - 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 (8 more)  
     
    Export citation  
     
    Bookmark  
  9.  21
    1 The Type Free Λρ-Calculus.Yuichi Komori & Arato Cho - 2002 - Bulletin of the Section of Logic 31 (2):65-70.
    Direct download  
     
    Export citation  
     
    Bookmark  
  10.  15
    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  
  11.  15
    Logic Based on Combinators.Yuichi Komori - 1989 - Bulletin of the Section of Logic 18 (3):100-104.