Works by Mitsuhiro Okada
24 found
Order:
1 filter applied
- The finite model property for various fragments of intuitionistic linear logic.Mitsuhiro Okada &Kazushige Terui -1999 -Journal of Symbolic Logic 64 (2):790-802.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 its intuitionistic version (ILLC). (...) The finite model property for related substructural logics also follow by our method. In particular, we shall show that the property holds for all of FL and GL - -systems except FL c and GL - c of Ono [11], that will settle the open problems stated in Ono [12]. (shrink)
- A Diagrammatic Inference System with Euler Circles.Koji Mineshima,Mitsuhiro Okada &Ryo Takemura -2012 -Journal of Logic, Language and Information 21 (3):365-391.Proof-theory has traditionally been developed based on linguistic (symbolic) representations of logical proofs. Recently, however, logical reasoning based on diagrammatic or graphical representations has been investigated by logicians. Euler diagrams were introduced in the eighteenth century. But it is quite recent (more precisely, in the 1990s) that logicians started to study them from a formal logical viewpoint. We propose a novel approach to the formalization of Euler diagrammatic reasoning, in which diagrams are defined not in terms of regions as in (...) the standard approach, but in terms of topological relations between diagrammatic objects. We formalize the unification rule, which plays a central role in Euler diagrammatic reasoning, in a style of natural deduction. We prove the soundness and completeness theorems with respect to a formal set-theoretical semantics. We also investigate structure of diagrammatic proofs and prove a normal form theorem. (shrink)
- Syntactic reduction in Husserl’s early phenomenology of arithmetic.Mirja Hartimo &Mitsuhiro Okada -2016 -Synthese 193 (3):937-969.The paper traces the development and the role of syntactic reduction in Edmund Husserl’s early writings on mathematics and logic, especially on arithmetic. The notion has its origin in Hermann Hankel’s principle of permanence that Husserl set out to clarify. In Husserl’s early texts the emphasis of the reductions was meant to guarantee the consistency of the extended algorithm. Around the turn of the century Husserl uses the same idea in his conception of definiteness of what he calls “mathematical manifolds.” (...) The paper argues that the notion anticipates the notion of reduction in term rewrite theory in computer science. The role of the reduction for Husserl is, however, primarily epistemological: its purpose is to impart clarity to formal mathematics. (shrink)
- Wittgenstein, Goodstein and the origin of the uniqueness rule for primitive recursive arithmetic.Mathieu Marion &Mitsuhiro Okada -2018 - In David G. Stern,Wittgenstein in the 1930s: Between the Tractatus and the Investigations. New York, NY: Cambridge University Press.
- 特集テーマ「タイプ理論」について.Mitsuhiro Okada -2021 -Kagaku Tetsugaku 53 (2):1.No categories
- Wittgenstein et le lien entre la signification d’un énoncé mathématique et sa preuve.Mathieu Marion &Mitsuhiro Okada -2012 -Philosophiques 39 (1):101-124.The thesis according to which the meaning of a mathematical sentence is given by its proof was held by both Wittgenstein and the intuitionists, following Heyting and Dummett. In this paper, we clarify the meaning of this thesis for Wittgenstein, showing how his position differs from that of the intuitionists. We show how the thesis originates in his thoughts, from the middle period, about proofs by induction, and we sketch his answers to a number of objections, including the idea that, (...) given the particular meaning he gives to this thesis, he cannot account for mathematical conjectures. We conclude by showing how his views find a favourable echo today in the paradigm of “proposition-as-type” and extensions of the Curry-Howard isomorphism from which this paradigm originates. (shrink)
- A Generalized Syllogistic Inference System based on Inclusion and Exclusion Relations.Koji Mineshima,Mitsuhiro Okada &Ryo Takemura -2012 -Studia Logica 100 (4):753-785.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.
- Remarks on logic for process descriptions in ontological reasoning: A Drug Interaction Ontology case study.Mitsuhiro Okada,Barry Smith &Yutaro Sugimoto -2008 - In Okada Mitsuhiro, Smith Barry & Sugimoto Yutaro, InterOntology. Proceedings of the First Interdisciplinary Ontology Meeting, Tokyo, Japan, 26-27 February 2008. Tokyo: Keio University Press. pp. 127-138.We present some ideas on logical process descriptions, using relations from the DIO (Drug Interaction Ontology) as examples and explaining how these relations can be naturally decomposed in terms of more basic structured logical process descriptions using terms from linear logic. In our view, the process descriptions are able to clarify the usual relational descriptions of DIO. In particular, we discuss the use of logical process descriptions in proving linear logical theorems. Among the types of reasoning supported by DIO one (...) can distinguish both (1) basic reasoning about general structures in reality and (2) the domain-specific reasoning of experts. We here propose a clarification of this important distinction between (realist) reasoning on the basis of an ontology and rule-based inferences on the basis of an expert’s view. (shrink)
- Some Remarks on a Difference between Gentzen's Finitist and Heyting's Intuitionist Approaches toward Intuitionistic Logic and Arithmetic.Mitsuhiro Okada -2008 -Annals of the Japan Association for Philosophy of Science 16 (1-2):1-17.
- A simple relationship between Buchholz's new system of ordinal notations and Takeuti's system of ordinal diagrams.Mitsuhiro Okada -1987 -Journal of Symbolic Logic 52 (3):577-581.
- Two Types of Demonstration Through Guided Touch with Cane: Instruction Sequences in Orientation and Mobility Training for a Person with Visual Impairments.Yasusuke Minami,Hiro Yuki Nisisawa,Mitsuhiro Okada &Rui Sakaida -2023 -Human Studies 46 (4):723-756.Persons with visual impairments (hereafter PVI) detect and discover obstacles and road conditions by touching with a white cane when walking on the streets. In one training session, an Orientation and Mobility specialist (hereafter SPT) guided a PVI by grasping and moving the cane that the PVI was holding. We conducted a multimodal analysis of two instruction sequences, one a "proving and achieving" demonstration (Sacks in Lectures on conversation, Blackwell, 1992) and the other a "learnable" (Zemel and Koschmann, in Discourse (...) Stud 16:163–183, 2014) demonstration. The achieving demonstration proved the assessment of the PVI's performance. In the "learnable" demonstration, the PVI was able to receive and perform the most critical part of the "learnable" of the long contact touch without the aid of talk. Sharing a single cane touch is an efficient way for both the guiding SPT and the guided PVI to jointly experience and understand the environmental features. The SPT did not need to verbally confirm that the guided touch was accountable to the PVI and seemed confident that intersubjectivity with the PVI had been established. A unique form of being with others and achieving intersubjectivity in society was identified. In traditional learning instruction, it has been assumed that the learnable is presented and communicated visually and audibly. However, through guided touch learnable is presented and conveyed effectively in the cases of this paper. It seems that the sense of touch has been considered to be just for the occasion, but this is an example of something that is not just for the occasion but is consequential, that is, usable for further occasions. The data is in Japanese. (shrink)No categories
- (1 other version)A direct independence proof of Buchholz's Hydra Game on finite labeled trees.Masahiro Hamano &Mitsuhiro Okada -1998 -Archive for Mathematical Logic 37 (2):67-89.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.
- A Relationship Among Gentzen's Proof‐Reduction, Kirby‐Paris' Hydra Game and Buchholz's Hydra Game.Masahiro Hamano &Mitsuhiro Okada -1997 -Mathematical Logic Quarterly 43 (1):103-120.We first note that Gentzen's proof-reduction for his consistency proof of PA can be directly interpreted as moves of Kirby-Paris' Hydra Game, which implies a direct independence proof of the game . Buchholz's Hydra Game for labeled hydras is known to be much stronger than PA. However, we show that the one-dimensional version of Buchholz's Game can be exactly identified to Kirby-Paris' Game , by a simple and natural interpretation . Jervell proposed another type of a combinatorial game, by abstracting (...) Gentzen's proof-reductions and showed that his game is independent of PA. We show that this Jervell's game is actually much stronger than PA, by showing that the critical ordinal of Jervell's game is φω = ϵ0) in the Veblen hierarchy of ordinals. (shrink)
- A weak intuitionistic propositional logic with purely constructive implication.Mitsuhiro Okada -1987 -Studia Logica 46 (4):371 - 382.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.
- Wittgenstein on Equinumerosity and Surveyability.Mathieu Marion &Mitsuhiro Okada -2014 -Grazer Philosophische Studien 89 (1):61-78.No categories
- Following a Rule: Waismann's Variation.Mathieu Marion &Mitsuhiro Okada -2018 - In Gabriele Mras, Paul Weingartner & Bernhard Ritter,Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium. Berlin, Boston: De Gruyter. pp. 359-373.No categoriesExport citation
Bookmark - Following a Rule: Waismann’s Variation.Mathieu Marion &Mitsuhiro Okada -2018 - In Gabriele Mras, Paul Weingartner & Bernhard Ritter,Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium. Berlin, Boston: De Gruyter. pp. 359-374.No categories
- Wittgenstein's struggle with intuitionism.Mathieu Marion &Mitsuhiro Okada -2023 - In Florian Franken Figueiredo,Wittgenstein's philosophy in 1929. New York, NY: Routledge.Export citation Bookmark
- A new correctness criterion for the proof nets of non-commutative multiplicative linear logics.Misao Nagayama &Mitsuhiro Okada -2001 -Journal of Symbolic Logic 66 (4):1524-1542.This paper presents a new correctness criterion for marked Danos-Reginer graphs (D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL. As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.
- Linear Logic and Intuitionistic Logic.Mitsuhiro Okada -2004 -Revue Internationale de Philosophie 4:449-481.
- On a theory of weak implications.Mitsuhiro Okada -1988 -Journal of Symbolic Logic 53 (1):200-211.
- Weak Logical Constants and Second Order Definability of the Full-Strength Logical Constants.Mitsuhiro Okada -1989 -Annals of the Japan Association for Philosophy of Science 7 (4):163-172.
- 帰納型消去規則としてのウィトゲンシュタインの一意性規則.Mitsuhiro Okada -2021 -Kagaku Tetsugaku 53 (2):95-114.No categories
- Genetic Factors of Individual Differences in Decision Making in Economic Behavior: A Japanese Twin Study using the Allais Problem.Chizuru Shikishima,Kai Hiraishi,Shinji Yamagata,Juko Ando &Mitsuhiro Okada -2015 -Frontiers in Psychology 6.
Off-campus access
Using PhilPapers from home?
Create an account to enable off-campus access through your institution's proxy server or OpenAthens.
Monitor this page
Be alerted of all new items appearing on this page. Choose how you want to monitor it:
 Email |  RSS feed |
Editorial team
General Editors:
David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Area Editors:
David Bourget
Gwen Bradford
Berit Brogaard
Margaret Cameron
David Chalmers
James Chase
Rafael De Clercq
Ezio Di Nucci
Esa Diaz-Leon
Barry Hallen
Hans Halvorson
Jonathan Ichikawa
Monte Johnson
Michelle Kosch
Øystein Linnebo
Paul Livingston
Brandon Look
Manolo Martínez
Matthew McGrath
Michiru Nagatsu
Susana Nuccetelli
Giuseppe Primiero
Jack Alan Reynolds
Darrell P. Rowbottom
Aleksandra Samonek
Constantine Sandis
Howard Sankey
Jonathan Schaffer
Thomas Senor
Daniel Star
Jussi Suikkanen
Aness Kim Webster
Other editors
Contact us
Learn more about PhilPapers
David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Area Editors:
David Bourget
Gwen Bradford
Berit Brogaard
Margaret Cameron
David Chalmers
James Chase
Rafael De Clercq
Ezio Di Nucci
Esa Diaz-Leon
Barry Hallen
Hans Halvorson
Jonathan Ichikawa
Monte Johnson
Michelle Kosch
Øystein Linnebo
Paul Livingston
Brandon Look
Manolo Martínez
Matthew McGrath
Michiru Nagatsu
Susana Nuccetelli
Giuseppe Primiero
Jack Alan Reynolds
Darrell P. Rowbottom
Aleksandra Samonek
Constantine Sandis
Howard Sankey
Jonathan Schaffer
Thomas Senor
Daniel Star
Jussi Suikkanen
Aness Kim Webster
Other editors
Contact us
Learn more about PhilPapers
Home |New books and articles |Bibliographies |Philosophy journals |About PhilPapers |API |Contact us |Code of conduct
PhilPapers logo byAndrea Andrews andMeghan Driscoll.
This site uses cookies and Google Analytics (see ourterms & conditions for details regarding the privacy implications).Use of this site is subject toterms & conditions.
All rights reserved byThe PhilPapers Foundation
Server: philpapers-web-54b44b69b7-vb4rf uwo