7 found
Sort by:
  1. Ryo Kashima (2003). On Semilattice Relevant Logics. Mathematical Logic Quarterly 49 (4):401.
    The semilattice relevant logics ∪R, ∪T, ∪RW, and ∪TW are defined by semilattice models in which conjunction and disjunction are interpreted in a natural way. For each of them, there is a cut-free labelled sequent calculus with plural succedents . We prove that these systems are equivalent, with respect to provable formulas, to the restricted systems with single succedents . Moreover, using this equivalence, we give a new Hilbert-style axiomatizations for ∪R and ∪T and prove equivalence between two semantics for (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. Kentaro Kikuchi & Ryo Kashima (2001). Sequent Calculi for Visser's Propositional Logics. Notre Dame Journal of Formal Logic 42 (1):1-22.
    This paper introduces sequent systems for Visser's two propositional logics: Basic Propositional Logic (BPL) and Formal Propositional Logic (FPL). It is shown through semantical completeness that the cut rule is admissible in each system. The relationships with Hilbert-style axiomatizations and with other sequent formulations are discussed. The cut-elimination theorems are also demonstrated by syntactical methods.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  3. Ryo Kashima & Norihiro Kamide (1999). Substructural Implicational Logics Including the Relevant Logic E. Studia Logica 63 (2):181-212.
    We introduce several restricted versions of the structural rules in the implicational fragment of Gentzen's sequent calculus LJ. For example, we permit the applications of a structural rule only if its principal formula is an implication. We investigate cut-eliminability and theorem-equivalence among various combinations of them. The results include new cut-elimination theorems for the implicational fragments of the following logics: relevant logic E, strict implication S4, and their neighbors (e.g., E-W and S4-W); BCI-logic, BCK-logic, relevant logic R, and the intuitionistic (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  4. Ryo Kashima (1997). Contraction-Elimination for Implicational Logics. Annals of Pure and Applied Logic 84 (1):17-39.
    We establish the “contraction-elimination theorem” which means that if a sequent Γ A is provable in the implicational fragment of the Gentzen's sequent calculus LK and if it satisfies a certain condition on the number of the occurrences of propositional variables, then it is provable without the right contraction rule. By this theorem, we get the following.1. If an implicational formula A is a theorem of classical logic and is not a theorem of intuitionistic logic, then there is a propositional (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  5. Ryo Kashima & Takeshi Yamaguchi (1997). On the Difficulty of Writing Out Formal Proofs in Arithmetic. Mathematical Logic Quarterly 43 (3):328-332.
    Let ℸ be the set of Gödel numbers Gn of function symbols f such that PRA ⊢ and let γ be the function such that equation imageWe prove: The r. e. set ℸ is m-complete; the function γ is not primitive recursive in any class of functions {f1, f2, ⃛} so long as each fi has a recursive upper bound. This implies that γ is not primitive recursive in ℸ although it is recursive in ℸ.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  6. Ryo Kashima (1994). Cut-Free Sequent Calculi for Some Tense Logics. Studia Logica 53 (1):119 - 135.
    We introduce certain enhanced systems of sequent calculi for tense logics, and prove their completeness with respect to Kripke-type semantics.
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  7. Ryo Kashima & Tatsuya Shimura (1994). Cut‐Elimination Theorem for the Logic of Constant Domains. Mathematical Logic Quarterly 40 (2):153-172.
    The logic CD is an intermediate logic which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen-type formulation called LD and rules are replaced by the corresponding intuitionistic rules) and that the cut-elimination theorem does not hold for LD. In this paper we present a modification of LD and prove the cut-elimination theorem for it. Moreover we prove a “weak” version of cut-elimination theorem for LD, saying that all “cuts” except (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation