[logic-ml] 「数学の哲学と証明論」ワークショップ、9月10日(木)-11日(金)、慶應義塾大学

Thu Sep 3 10:13:01 JST 2015

慶應義塾大学非常勤講師の高橋優太と申します。

ワークショップ「数学の哲学と証明論」のご案内をお送りいたします。ぜひご参加ください。

---------------------------------------------------------------------
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 事務局
logic at abelard.flet.keio.ac.jp
---------------------------------------------------------------------

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20150903/030c6fcf/attachment-0001.html>