慶應義塾大学非常勤講師の高橋優太と申します。
ワークショップ「数学の哲学と証明論」のご案内をお送りいたします。ぜひご参加ください。
--------------------------------------------------------------------- We apologize if you receive this message more than once. ---------------------------------------------------------------------
カーネギーメロン大学W.Sieg教授をお招きして次のようなワークショップ 「Philosophy of Mathematics and Proof Theory」を予定しております。参加自由です。 （なお、次回はG-Y Girard教授をお招きして、11月28日-29日に開催する予定です。 Sieg教授は9月18日にも早稲田大学で別テーマの講演をなさいます。 URL:http://www.waseda.jp/wias/event/symposium/sym_150918.html ）
----
"Philosophy of Mathematics and Proof Theory" Workshop 「数学の哲学と証明論」ワークショップ
Date: September 10th(Thu)-21th(Fri), 2015 日時: 2015年9月10日(木)-11日(金) Place: Hall (8F), East Building, Mita campus of Keio University. 場所: 慶應大学三田キャンパス 東館8階ホール (http://www.keio.ac.jp/en/maps/mita.html )
講演アブストラクトを始め会議のupdated informationについてはつぎのURLをご覧ください。 http://abelard.flet.keio.ac.jp/seminar/sieg2015.html
----
Tentative Program:
9/10:
13:00-13:10 Opening Remark, Mitsuhiro Okada and Ryota Akiyoshi
13:00-14:00 Kengo Okamoto (Tokyo Metropolitan University) "TBA"
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 $\Pi^{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
9/11:
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
---------------------------------------------------------------------
Organisers: Mitsuhiro Okada (co-chair) Ryota Akiyoshi (co-chair) Yutaro Sugimoto Yuta Takahashi
主催: 三田ロジックセミナー 共催: 慶應義塾大学 論理と感性のグローバル研究センター
問合せ先: Mita Logic Seminar 事務局 [email protected] ---------------------------------------------------------------------
ABSTRACTS
9/10:
Mamoru Kaneko (Waseda University) "Game Theoretic Decidability and Undecidability" (with Tai-Wei Hu) Abstract: 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² (a fixed-point extension) of the epistemic logic KD² to capture individual decision making from the viewpoint of logical inference. In the logic EIR², 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²;Δ_{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.
Ryota Akiyoshi (Waseda Institute for Advanced Study): "Some results in proof-theory for $\Pi^{1}_{1}$-$CA$" Abstract: In 2000's, Tait asked the question whether we can prove without ordinal notations that all proofs in $\Pi^{1}_{1}$-$CA$ with (Sch"{u}tte's) $\omega$-rule are transformed into cut-free ones. Inspired by this, the author and Mints formulated an extension of Buchholz' $\Omega$-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 $\Omega$-rule. In the first part of the talk, we will explain the result with Mints.
Next, we explain a connection between the $\Omega$-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 $\Omega$-rule in the framework of the computability. We report and discuss our result.
Wilfried Sieg (Carnegie Mellon University) "Dedekind's structuralism: creating concepts and deriving theorems" Abstract: 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.)
9/11:
Yuta Takahashi (Keio University) "Gentzen's 1935/36 Consistency Proofs as Means of Ascribing Constructive Senses" Abstract: 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.
Mitsuhiro Okada (Keio University) "Husserl's universal arithmatic and his proof theoretical view of formal mathematics" Abstract: 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).
Wilfried Sieg (Carnegie Mellon University) "The ways of Hilbert's axiomatics: structural and formal" Abstract: 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.