-
1Wittgenstein's struggle with intuitionismIn Florian Franken Figueiredo (ed.), Wittgenstein's philosophy in 1929, Routledge. 2023.
-
6Persons 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" (Z…Read more
-
27Wittgenstein on Equinumerosity and SurveyabilityGrazer Philosophische Studien 89 (1): 61-78. 2014.
-
54Wittgenstein et le lien entre la signification d’un énoncé mathématique et sa preuvePhilosophiques 39 (1): 101-124. 2012.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…Read more
-
13Following a Rule: Waismann’s VariationIn Gabriele Mras, Paul Weingartner & Bernhard Ritter (eds.), Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium, De Gruyter. pp. 359-374. 2019.
-
71Syntactic reduction in Husserl’s early phenomenology of arithmeticSynthese 193 (3): 937-969. 2016.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 “mathemati…Read more
-
InterOntology. Proceedings of the First Interdisciplinary Ontology Meeting, Tokyo, Japan, 26-27 February 2008Keio University Press. 2008.
-
Following a Rule: Waismann's VariationIn Gabriele Mras, Paul Weingartner & Bernhard Ritter (eds.), Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium, De Gruyter. pp. 359-373. 2019.
-
224We 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 o…Read more
-
Proceedings of the Conference on Ontology and Analytical Metaphysics, February 24-25, 2011 (edited book)Keio University Press. 2011.
-
15Some Remarks on a Difference between Gentzen's Finitist and Heyting's Intuitionist Approaches toward Intuitionistic Logic and ArithmeticAnnals of the Japan Association for Philosophy of Science 16 (1-2): 1-17. 2008.
-
17A Direct Independence Proof of Buchholz's Hydra Game on Finite Labeled TreesBulletin of Symbolic Logic 7 (4): 534-535. 2001.
-
8A Proof-theoretic Study Of The Correspondence Of Classical Logic And Modal LogicJournal of Symbolic Logic 68 (4): 1403-1414. 2003.It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg proved this fact in a syntactic way. Mints extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints’ result to the basic modal logic S4; we investigate the correspondence …Read more
-
Essays in the Foundations of Logical and Phenomenological Studies (Interdisciplinary Series on Reasoning Studies, Vol. 3) (edited book)Keio University. 2007.
-
Ontology and Phenomenology: Franco-Japanese Collaborative Lectures (edited book)Keio University. 2009.
-
37A proof–theoretic study of the correspondence of hybrid logic and classical logicJournal of Logic, Language and Information 16 (1): 35-61. 2006.In this paper, we show the equivalence between the provability of a proof system of basic hybrid logic and that of translated formulas of the classical predicate logic with equality and explicit substitution by a purely proof–theoretic method. Then we show the equivalence of two groups of proof systems of hybrid logic: the group of labelled deduction systems and the group of modal logic-based systems.
-
73A proof-theoretic study of the correspondence of classical logic and modal logicJournal of Symbolic Logic 68 (4): 1403-1414. 2003.It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the corres…Read more
-
82The finite model property for various fragments of intuitionistic linear logicJournal 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
-
60A Generalized Syllogistic Inference System based on Inclusion and Exclusion RelationsStudia 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
-
49A weak intuitionistic propositional logic with purely constructive implicationStudia 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.
-
59A direct independence proof of Buchholz's Hydra Game on finite labeled treesArchive 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.
-
15The Finite Model Property for Various Fragments of Intuitionistic Linear LogicJournal of Symbolic Logic 64 (2): 790-802. 1999.Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic and for affine logic, 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, and intuitionistic LLW. In addition, we shall show the finite model property for contractive linear logic, i.e., linear logic with contraction, and for its intuitionistic version. The finite model property for rel…Read more
-
57A new correctness criterion for the proof nets of non-commutative multiplicative linear logicsJournal of Symbolic Logic 66 (4): 1524-1542. 2001.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
-
25A Relationship Among Gentzen's Proof‐Reduction, Kirby‐Paris' Hydra Game and Buchholz's Hydra GameMathematical Logic Quarterly 43 (1): 103-120. 1997.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 abstra…Read more
-
34Weak Logical Constants and Second Order Definability of the Full-Strength Logical ConstantsAnnals of the Japan Association for Philosophy of Science 7 (4): 163-172. 1989.
-
11A New Correctness Criterion For The Proof Nets Of Non-commutative Multiplicative Linear LogicsJournal of Symbolic Logic 66 (4): 1524-1542. 2001.This paper presents a new correctness criterion for marked Danos-Reginer graphs 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.