「数学の哲学と証明論」ワークショップ

- Date:
- September 10th–11th, 2015 / 日時: 2015年9月10日(木)–11日(金)
- Place:
- The 8F hall of the east building, mita campus of Keio University
- 場所:
- 慶應義塾大学三田キャンパス東館8階ホール
- Map:
- http://www.keio.ac.jp/en/maps/mita.html

Program:

Thursday, September 10th

- 13:00-13:10
- Opening Remark, Mitsuhiro Okada & Ryota Akiyoshi
- 13:10-14:00
- Kengo Okamoto (Tokyo Metropolitan University)

“Intuitionistic provability, classical validity and situation-dependent propositions – A consideration based onGödel’s modal embedding (reivised)” - 14:00-15:00
- Mamoru Kaneko (Waseda University)

“Game Theoretic Decidability and Undecidability” (with Tai-Wei Hu) - 15:00-15:20
- Break
- 15:20-16:20
- Ryota Akiyoshi (Waseda Institute for Advanced Study)

“Some results in proof-theory for Π_{1}^{1}-CA” - 16:20-17:50
- Wilfried Sieg (Carnegie Mellon University)

“Dedekind’s structuralism: creating concepts and deriving theorems” - 17:50-18:20
- Discussion

Friday, September 11th

- 13:30-14:20
- Yuta Takahashi (Keio University)

“Gentzen’s 1935/36 Consistency Proofs as Means of Ascribing Constructive Senses” - 14:20-15:00
- Mitsuhiro Okada (Keio University)

“Husserl’s universal arithmatic and his proof theoretical view of formal mathematics” - 15:00-15:20
- Break
- 15:20-16:50
- Wilfried Sieg (Carnegie Mellon University)

“The ways of Hilbert’s axiomatics: structural and formal” - 16:50-17:20
- Concluding Discussion

We study the possibility of prediction/decision making in a finite 2–person game with pure strategies, following the Nash-Johansen noncooperative solution theory. We adopt the infinite-regress logic EIR^{2} (a fixed-point extension) of the epistemic logic KD^{2} to capture individual decision making from the viewpoint of logical inference.
In the logic EIR^{2}, prediction/decision making is described by the belief set Δ_{i}(g) for player i, where g specifies a game.
Our results on prediction/decision making differ between solvable and unsolvable games.
For the former, we show that player i can decide whether each of his strategies is a final decision or not. For the latter, we obtain undecidability, i.e., he can neither decide some strategy to be a possible decision nor disprove it. Thus, the theory (EIR^{2};Δ_{i}(g)) is incomplete in the sense of Gödel’s incompleteness theorem for an unsolvable game g. This result is related to “self-referential”, but its main source is a discord generated by interdependence of payoffs and independent prediction/decision making.

In 2000’s, Tait asked the question whether we can prove without ordinal notations that all proofs in Π_{1}^{1}-CA with (Schütte’s) ω-rule are transformed into cut-free ones. Inspired by this, the author and Mints formulated an extension of Buchholz’ Ω-rule using Takeuti’s distinction of explicit/implicit inference and proved the complete cut-elimination theorem for it. An answer to Tait’s question is given by combining this with the author’s work on "finite notations for infinitary derivations" for this kind of Ω-rule. In the first part of the talk, we will explain the result with Mints.

Next, we explain a connection between the Ω-rule and the computability predicate by Tait-Girard. In 2008, Mints suggested that there should be a connection between these two methods because they would have a common aim to solve the difficulty how to deal with the substitution of a set term T into a free second-order variable X in A(X). The author and Terui recently found this connection by formulating the Ω-rule in the framework of the computability. We report and discuss our result.

Dedekind’s structuralism is a crucial source for the structuralism of mathematical practice with its focus on abstract concepts like groups and fields. It plays an equally central role for the structuralism of philosophical analysis with its focus on particular mathematical objects like natural and real numbers. Tensions between these structuralisms are palpable in Dedekind’s work, but are resolved in his essay Was sind und was sollen die Zahlen?

In a radical shift, Dedekind extends his mathematical approach to “the” natural numbers. He creates the abstract concept of a simply infinite system, proves the existence of a “model”, insists on the stepwise derivation of theorems, and defines structure-preserving mappings between different systems that fall under the abstract concept. Crucial parts of these considerations were added only to the penultimate manuscript, for example, the very concept of a simply infinite system.

The methodological consequences of this radical shift are elucidated by an analysis of Dedekind’s metamathematics. Our analysis provides a deeper understanding of the essay and, in addition, illuminates its impact on the evolution of the axiomatic method and of “semantics” before Tarski. This understanding allows us to make connections to contemporary issues in the philosophy of mathematics and science. (This reports on work with Rebecca Morris.)

Gentzen’s three consistency proofs for number theory have a common aim that originates from Hilbert’s Program, namely, the aim to justify the application of classical reasoning to quantified propositions in number theory. In addition to this common aim, Gentzen gave a constructive interpretation to every number-theoretic proposition in his 1935/36 consistency proofs, while Hilbert’s Program included no such interpretation. In this talk, we claim that Gentzen’s interpretation took a part of his response to an objection posed by Brouwer against the significance of consistency proofs. Specifically, we argue as follows. According to Brouwer, consistency proofs for classical mathematics are of no significance, because its theorems have no sense whether or not its consistency is proved by using the methods of the Hilbert School. In order to respond to this objection, Gentzen aimed at ascribing a constructive sense to each theorem of classical number theory by means of his interpretation.

We discuss Husserl’s development of the conception of universal arithmatic, with the special focus on his Double-Lecture and other manuscripts in 1901. We can see how his work is influenced from former formalists’ work and, at the same time, how it is sharply contrasted to those such as Hankel’s and Hilbert’s former work. We discuss Husserl’s view of proof-theoretic and computational notion of “manifold” (in his own sense), and his term-rewrite theoretic notion of “definiteness” of manifold. We also discuss some significance of the Husserlian proof theoretic view of mathematics as well as some limitation (for which Wittgenstein partly solved much later).

It is a remarkable fact that Hilbert’s programmatic papers from the 1920s still shape, almost exclusively, the standard contemporary perspective of his views concerning (the foundations of) mathematics; even his own, quite different work on the foundations of geometry and arithmetic from the late 1890s is often understood from that vantage point. My essay pursues one main goal, namely, to contrast Hilbert’s formal axiomatic method from the early 1920s with his existential axiomatic approach from the 1890s, deeply influenced by Dedekind.

Such a contrast illuminates the circuitous beginnings of the finitist consistency program and connects the complex emergence of existential axiomatics with transformations in mathematics and philosophy during the 19th century; the sheer complexity and methodological difficulties of the latter development are partially reflected in the well known, but not well understood correspondence between Frege and Hilbert. Taking seriously the goal of formalizing mathematics in an effective logical framework leads also to contemporary tasks, not just historical and systematic insights.

主催：三田ロジックセミナー

共催：慶應義塾大学「論理と感性」のグローバルリサーチセンター

平成27年度科学研究費助成事業 新学術領域研究(研究領域提案型)

三田ロジックセミナー 事務局 : E-Mail : logic [AT] abelard.flet.keio.ac.jp

This document was translated from L^{A}T_{E}X byH^{E}V^{E}A.