French-Japanese Workshop “Philosophy of Logic and Mathematics”
with special focuses on "Philosophy of Proofs" and the Study of Euclid's Elements



Jan 19th Friday-20th Saturday, 2018 / 2018年1月19日(金) 9:50-18:30 20日(土) 9:50 - 17:10
Distance Learning Room (B4F), South Building, Mita Campus of Keio University / 慶應義塾大学三田キャンパス 南館地下4階 ディスタンスラーニングルーム
Building #12 on this map. / キャンパスマップ12番の建物です。
Guest Speakers from France
  1. Marco Panza (Univ. Paris-1 and IHPST)
    What Universality Could Have Been for Euclid
  2. Pierre Wagner (Univ. Paris-1 and IHPST)
    Logical Commitment
  3. Andrew Arana (Univ. Paris-1 and IHPST)
    Syntactic purity and normalization(Joint work with Mitsu Okada)
  4. Jean-Baptiste Joinet (Univ. Lyon-3 and Inst. Jean Cavaillès (ENS-Paris))
    On agonal ontologies
Guest Speakers from Japan
  1. 斎藤 憲 Ken Saito (Osaka Prefecture Univ.)
    Syntax Analysis of the Whole Text of Euclid’s Elements
  2. Nathan Camillo Sidoli (Waseda Univ.)
    Euclid’s Postulates and Problems
  3. 伊藤 遼 Ryo Ito (Univ. of Kyoto)
    The Unity of the Proposition and Russell's Theories of Truth
Japanese Group Speakers and Other Speakers
  1. 秋吉 亮太 Ryota Akiyoshi (Waseda Univ.)
    “Proofs as Programs” Revisited
  2. Daniel Said Monteiro (Univ. Paris 7 and Keio Univ.)
    Explaining the movements of qi: Nishikawa Joken (1648-1724) and the understanding of extraordinary phenomena in early modern Japan
  3. 張 峻豪 CHANG Chun Hao (National Tsing Hua Univ.)
    The quantification of differences of diagrams in proofs by contradiction
  4. 小関 健太郎 Kentaro Ozeki (Keio Univ.)
    Meinongian Incomplete Objects and Negation
  5. 西牟田 祐樹 Yuki Nishimuta (Keio Univ.)
    Generalized Connectives, Validity of Cut and Deducibility of Identicals (preliminary report)
  6. 山﨑 紗紀子 Sakiko Yamasaki (Tokyo Metropolitan Univ.)
    Constructive proof of Gödel-McKinsey-Tarski Theorem via Multi-succedent G3-Style Sequent Calculus for Intuitionistic Logic
  7. 岡田 光弘 Mitsuhiro Okada (Keio Univ.)
    Norm, Commitment and Normalization of Proof (tentative)

And others to be announced



First Day. Jan 19th (Friday)

  • 9:50 Registration
  • Session I : History and philosophy of Euclid’s Elements Part 1
    • 10:00 introduction
    • 10:10 Nathan Camillo Sidoli (Waseda Univ.)
      “Euclid’s Postulates and Problems”

      In this talk I will differentiate between the way that constructions are used in problems and in theorems in the plane books of Euclid's Elements problem-constructions and proof-constructions. I will then show how the concept of given, as developed in the Data, can be used to explicate all five Euclidean postulates, and to show how these postulates are used in problems. Finally, I will discuss the detailed syntax of a Euclidean problem-construction and show that this is rather different that usually described as a construction with compass and straightedge.

    • 11:10 斎藤 憲 Ken Saito (Osaka Prefecture Univ.)
      “Syntax analysis of the whole text of Euclid's Elements

      I present an ongoing project of syntactic analysis of the whole Greek text of Euclid's Elements (about 150,000 words). Its goal is construction of stemma for each sentence of this work.

      The Elements are written in a natural language (ancient Greek). Though the text is quite monotonous, one can sometimes discern subtle stylistic oscillations, so that one can expect that a thoroughgoing syntactic analysis might reveal different origins of different parts of this work. The grammatical rules at the base of the analysis are modelled after Tesnière's dependency grammar. A computer program is under development which helps the analysis suggesting applicable rules to the word the user selects, and saves the results.

      The Elements are the most known, read and commented work of Greek mathematics since antiquity, and it is now difficult to identify the original parts from later additions, for our sources are limited to Byzantine manuscripts (9th century onward) and Arabo-Latin translations (although the latter sometimes reveal later interventions not discernible in Greek tradition).

      A syntactically analyzed text of the whole Elements (searchable by any conceivable conditions) would greatly advance our understanding of ancient Greek mathematics, helping the distinction of various components with different origins mixed in the extant Greek text of the Elements.

    • 12:10-12:30 Discussion
    • 12:30-14:00 Lunch Break
  • Session II : History and philosophy of Euclid’s Elements Part II
    • 14:00 Marco Panza (Univ. Paris-1 and IHPST)
      “What Universality Could Have Been for Euclid” An Appendix Session on history of Japanese Science”

      A classical problem concerning Euclid¹s geometry concerns the contrast between the apparent particularity of its proofs and the apparent generality of its propositions.
      It will be argued that:
      1) no philological enquiry can alone solve the problem, since what is needed to this purpose is reconstructing the internal logic of Euclid¹s theory;
      2) Despite appearances, Euclid¹s proof are, in fact, as general as they could have been, in agreement with this logic.

    • 15:00 Daniel Said Monteiro (Univ. Paris 7 and Keio Univ.)
      “Explaining the movements of qi: Nishikawa Joken (1648-1724) and the understanding of extraordinary phenomena in early modern Japan”
      Nishikawa Joken, a Confucian scholar from Nagasaki, is mostly known for his writings on astronomy. Among his works, the Kaii bendan 怪異辨斷 (“Explanation of [things] extraordinary”) stands out as a compilation of literary and historical sources that mention extraordinary phenomena occurring in the skies and on earth, with an appended commentary by Joken to each citation.
      The Keio Institute of Oriental Classics holds a manuscript that appears to be the third and final part of the Kaii bendan, with the title of Kaii ruisan 怪異類纂 (“Compilation of [things] extraordinary”). This works has a similar structure, but contains quoted passages about extraordinary phenomena concerning the human body.
      In my presentation, I will discuss the importance of the Kaii ruisan manuscript - which seems to be the sole surviving catalogued copy of this work - in light of its connection to the more widely available Kaii bendan. My aim is to exemplify how the understanding of the natural sciences in early modern Japan had its foothold on the ancient Chinese cosmological conception that the heavenly, earthly and human phenomena (tenchijin 天地人) are inextricably connected.
    • 15:30-15:50 Discussion & coffee break
  • Session III : Philosophy of logic and ontology
    • 15:50 Jean-Baptiste Joinet (Univ. Lyon-3 and Inst. Jean Cavaillès (ENS-Paris))
      “On agonal ontologies”

      In Frege and Russell’s line, the main tool to propagate ontology toward higher orders is realized by quotienting sets by equivalence relations. Indeed, this leads to produce, at the next order, separated individuals (disjoint non empty subsets covering the original set) and this in such a way that this separation is conceptually generated from a relation at the initial order.

      This way to relate ontology and equivalence relations is Parmenidian in inspiration, non only because it considers individuals independently of time, but also because it is deeply found upon the idea of sameness. The important point with this respect is not so much that individualities at the new order reflect a similarity at the previous order, but the fact that a given individuality at the new order depends only of itself (i.e. of the relational commitment of its own members) and in particular is independent of other individualities (i.e. of the relational commitment of members of other classes).

      In my last talk in Keio (in April 2017), I defended the view that "Denotational semantics of programs" (the research programme launched by Strachey and Scott around 1969) can be seen as a first step to substitute to Parmenidian ontology an Heraclitean ontology, in the sense that it faces the first point (individuals in time): in a computational universe, transformation comes first and separation phenomenas are generated by (and compatible with) these transformation.

      In the present talk, my aim is to present a complementary program toward an heraclitean ontological point of view, agonal ontology, facing the second point.

    • 16:50 伊藤 遼 Ryo Ito (Univ. of Kyoto)
      “The Unity of the Proposition and Russell’s Theory of Truth”
      From 1898 onwards Bertrand Russell developed his ontology of propositions, where propositions are considered to be mind-independent complexes. By the time the first volume of Principia Mathematica was finally published, however, he abandoned the ontology without offering any convincing arguments for doing so. Some philosophers have explained it was because he found that his account of the unity of a proposition would make it impossible to make a false judgment. I will argue, contra those philosophers, that the alleged impossibility itself cannot explain why he changed his view, as their argument involves an assumption that was alien to Russell’s ‘qualitative’ account of truth and falsehood. I will then move on to illustrate, though briefly, how he became unsatisfied with the qualitative account in favour of an ‘existential’ account of truth, which resulted in the abandonment of the ontology of propositions.
    • 17:50 小関 健太郎 Kentaro Ozeki (Keio Univ.)
      “Meinongian Incomplete Objects and Negation”
      Some objects are not completely determined with regard to certain properties: Lockean general idea of triangle, the universal “chair”, fictional entities, and so on. In consequence of the Russell-Meinong debate on impossible objects, Meinong introduced two types of negation, so-called internal (term) negation and external (sentential) negation, which were eventually applied to his theory of incompletely determined objects and the law of excluded middle. In my talk, I discuss these two types of negation and their logical-ontological relationship to the treatment of incomplete objects in Meinongian semantics. While several interpretations are possible in connection with negative properties and/or negative state of affairs (objectives), I argue that both internal and external negation should be considered in terms of objectives.
    • 18:20-18:30 Discussion
    • 18:30 Closing of the first day program

Second Day. Jan 20th (Saturday)

  • 9:50 Registration
  • Session IV : The Project-thematic Session on Philosophy of Logic
    • 10:00 Pierre Wagner (Univ. Paris-1 and IHPST)
      “Logical Commitment”
      In his 2004 paper ("In what sense (if any) is logic normative for thought?"), John MacFarlane lauched a debate on the normativity of logic. In this debate, people have met the separate issue of the plurality of logic (in what sense, if any, is logic normative if there is a plurality of equally correct logics?). Now it is by no means obvious that MacFarlane's central notion of "bridge principles" (between logical claims and norms of reasoning) will provide a satisfatory answer to the issue of pluralism. In this paper, it is argued that the debate on logical pluralism and normativity will have to take into accound a notion of logical commitment which has not been discussed so far in this context.
    • 11:00 岡田 光弘 Mitsuhiro Okada (Keio Univ.)
      “Norm, Commitment and Normalization of Proof (tentative)”

      We discuss how a proof can be accepted or rejected as a normal proof. From this view point we consider the role of normalization of proofs, as well as re-normalization of them. We relate this consideration to Cartesian normalization, Husserlian normalization, Hilbert-Gentzen re-normalization, Wittgensteian normalization, of proofs/demonstrations.

    • 11:30 Andrew Arana (Univ. Paris-1 and IHPST)
      “Syntactic purity and normalization”(Joint work with Mitsu Okada)
      Roughly, a proof of a theorem, is pure if it draws only on what is “close” or “intrinsic” to that theorem. There are now several different ways of measuring “closeness” in the literature. In a 2009 article I introduced a syntactic measure of purity in which what is close to a theorem are the subformulas of its statement. Theories that admit cut elimination can then be seen to admit pure proofs, in this sense, of every theorem. Valuable though this may be, its range is rather limited, as cut elimination fails to hold in general for systems with non-logical axioms. In this talk, I want to push this question further by considering other normal forms for proofs than being cut-free, and developing syntactic measures of purity using these normal forms. In particular, I want to consider Knuth-Bendix completion as a normal form, and evaluate confluence as a condition ensuring the existence of pure proofs. This will lead to the general question: for a given logical system, can a syntactically impure proof always be replaced with a pure proof? One can call such systems “purifiable” and one can ask which systems are purifiable, as well as what the value of pure proofs in such systems would be.
    • 12:30-12:40 Discussion
    • 12:40-14:10 Lunch Break
  • Session V : Philosophycal and Historical Studies on Proofs
    • 14:10 張峻豪 Chang Chun Hao (National Tsing Hua Univ.)
      “The quantification of differences of diagrams in proofs by contradiction”
      Some recent studies have shown that manuscript diagrams of Euclidean Elements can be far different from the diagrams made by modern editors or mathematicians. For instance, Saito (2012) had a general summary of the characteristics of Greek manuscript diagrams. However, the judgements concerning the differences of diagrams are usually based upon the “feelings” of visual objects. In order to build other supporting evidence, I made a trial for the quantification of the differences of diagrams on the basis of an observation: In the proofs by contradiction found in the Elements, there is always a comparison between two angles, lengths or areas right before the sentence “The very thing is impossible.” I collected some diagrams of proofs by contradiction from Book I and III in 16 editions of the Elements, including Greek manuscripts and early modern printed editions, and calculated the ratios of the aforementioned comparison, which I call “contradiction degree.” The main result of this quantification is that the values of “contradiction degree” for manuscript diagrams are considerably larger than those for the diagrams in printed editions. I will discuss whether manuscript diagrams present an ancient tradition of visual representation and the other possible interpretations that this result can suggest.
    • 14:40 岡田 光弘 Mitsuhiro Okada (Keio Univ.) and Yuta Takahashi (Nagoya Univ. and JSPS)
      “Ordinal Diagrams and Well-Quasi-Orderings (preliminary report)”
    • 15:10 山﨑 紗紀子 Sakiko Yamasaki (Tokyo Metropolitan Univ.)
      “Constructive proof of Gödel-McKinsey-Tarski Theorem via Multi-succedent G3-Style Sequent Calculus for Intuitionistic Logic”
      In this presentation, I shall first present the multi-succedent G3-style sequent calculus for intuitionistic logic. Then, a new constructive proof of Gödel-McKinsey-Tarski Theorem in terms of that calculus is presented. Finally, I will try to suggest that we thereby obtain several technically very general and philosophically interesting outlooks on Gödel-McKinsey-Tarski embedding.
    • 15:40-16:00 Discussion & coffee break
  • Session VI : Philosophy of Proofs and Proof Theory
    • 16:00 秋吉 亮太 Ryota Akiyoshi (Waseda Univ.)
      “Proofs as Programs” Revisited

      Schwichtenberg has developed the program called “Proofs as Programs" by measuring the “complexity as programs” of proofs in an arithmetical system (with recursion). Technically, he used a slow growing hierarchy to “clime down” tree ordinals, which are introduced by Buchholz. This observation is due to Arai and is going back to Girard’s “Hierarchy comparison theorem”.

      In this talk, we sketch a new approach to this program by focusing on parameter-free subsystems of Girard’s F. There are at least two advantages in this approach. (i) Our approach is simpler and smoother than the original one. (ii) It is relatively easy and uniform to extend our results to stronger fragments (corresponding to iterated inductive definitions) though the theory analysed by Schwichtenberg has the strength of Peano Arithmetic.

      This work is based on joint work with Schwichtenberg.

    • 16:30 西牟田 祐樹 Yuki Nishimuta (Keio Univ.)
      “Generalized Connectives, Validity of Cut and Deducibility of Identicals (preliminary report)”

      In this talk, we consider the validity of cut. One natural criterion for the validity of cut which contains a connective C is that the main reduction step for C is defined. (Danos and Regnier, 1989) introduced generalized multiplicative connectives that cannot be defined by combinations of binary multiplicative connectives in a fragment of Linear Logic. The validity of cut for these connectives is defined by the cut-eliminability of them. We show that the validity of cut via cut-eliminability does not guarantee the compositionality of the validity in a model (i.e. soundness of the cut rule). We also show that if a connective C satisfies the deducibility of identical condition introduced in (Hacking, 1979) (or the uniqueness condition introduced in (Belnap, 1962)) in addition to the cut-eliminability, the validity of cut guarantees the compositionality of the validity in a model.

    • 17:00 Concluding Discussion
    • 17:10 Closing
  • 岡田 光弘 (慶應義塾大学) [責任者]
  • 小関 健太郎(慶應義塾大学)
  • 高橋 優太 (名古屋大学・日本学術振興会)
  • 西牟田 祐樹 (慶應義塾大学)
  • 慶應義塾大学論理と感性のグローバル研究センター
  • 次世代研究推進プロジェクト
  • CNRS(フランス)
慶應義塾大学文学部 岡田光弘研究室
Email: logic [AT] abelard.flet.keio.ac.jp