profile picture

Mitsuhiro Okada

 More details
  •  83
    The finite model property for various fragments of intuitionistic linear logic
    with Kazushige Terui
    Journal of Symbolic Logic 64 (2): 790-802. 1999.
    Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction, and for…Read more
    Nonclassical LogicsProof Theory
  •  60
    A Generalized Syllogistic Inference System based on Inclusion and Exclusion Relations
    with Koji Mineshima and Ryo Takemura
    Studia Logica 100 (4): 753-785. 2012.
    We introduce a simple inference system based on two primitive relations between terms, namely, inclusion and exclusion relations. We present a normalization theorem, and then provide a characterization of the structure of normal proofs. Based on this, inferences in a syllogistic fragment of natural language are reconstructed within our system. We also show that our system can be embedded into a fragment of propositional minimal logic
    Logics, MiscProof Theory
  •  50
    A weak intuitionistic propositional logic with purely constructive implication
    Studia Logica 46 (4). 1987.
    We introduce subsystems WLJ and SI of the intuitionistic propositional logic LJ, by weakening the intuitionistic implication. These systems are justifiable by purely constructive semantics. Then the intuitionistic implication with full strength is definable in the second order versions of these systems. We give a relationship between SI and a weak modal system WM. In Appendix the Kripke-type model theory for WM is given.
    Intuitionistic LogicProof Theory
  •  59
    A direct independence proof of Buchholz's Hydra Game on finite labeled trees
    with Masahiro Hamano
    Archive for Mathematical Logic 37 (2): 67-89. 1998.
    We shall give a direct proof of the independence result of a Buchholz style-Hydra Game on labeled finite trees. We shall show that Takeuti-Arai's cut-elimination procedure of $(\Pi^{1}_{1}-CA) + BI$ and of the iterated inductive definition systems can be directly expressed by the reduction rules of Buchholz's Hydra Game. As a direct corollary the independence result of the Hydra Game follows.
    Proof Theory