PROOF THEORY AND PHILOSOPHY
Feb 26th, 2011, Tokyo, Keio University, Mita Campus
「証明論の展開とその哲学」シンポジウム
2011年2月26日(土) 慶應義塾大学三田キャンパス

現代論理学、特に証明論から引き出された文脈のなかで、Hilbert, Gödel, Friedman, Girard らによって議論されたテーマのいくつかついて、その技術的概観とともに哲学的観点を検討することを本研究会の目的としています。

The purpose of this Meeting is to discuss issues presented in various new fields derived from proof theory, initiated by Hilbert, Gëdel, Friedman, Girard and others, from the philosophical point of view as well as from the technical point of view.



日時
2011年2月26日(土) 13:00-18:00
Date:
13:00-18:00 Feb 26th, 2011
場所:
慶應義塾大学 三田キャンパス 東館6階 G-Sec Lab
Place:
G-Sec Lab, 6th floor of the East Building, the Mita Campus, Keio University
URL:
http://abelard.flet.keio.ac.jp/ptp11/

1.
Richard Zach (University of Calgary, Department of Philosophy)
“Gëdel’s First Incompleteness Theorem and Mathematical Instrumentalism”
2.
Ryo Takemura (Keio University)
“Proof theory for reasoning with Euler diagrams”
3.
Sam sanders (Ghent University and Tohoku University)
“Reverse Mathematics & Non-Standard Analysis: WHY SOME THEOREMS ARE MORE EQUAL THAN OTHERS
4.
Michele Basaldella (Kyoto University)
“A gentle introduction to ludics”

18:15-
Reception Party at Chuugoku Hanten Restaurant near (a few minutes walk distance from) the conference site/EAST GATE of the Mita Campus (Free for participation) 懇親会 (於 中国飯店) 参加自由無料です.

Gödel’s First Incompleteness Theorem and Mathematical Instrumentalism
Richard Zach (Calgary University )

Abstract: According to instrumentalist views of mathematics, only certain mathematical propositions are straightforwardly meaningful, whereas much of mathematics is only a useful tool. Instrumentalism in mathematics is attractive since this view avoids ontological commitment to those mathematical entities the merely useful part of mathematics is quantifiying over. David Hilbert’s foundational program of the 1920s is often read as involving such a brand of instrumentalism: only the finitary part of mathematics is meaningful, the rest – “ideal” mathematics – is not, and its use was supposed to be legitimated by a finitary consistency proof. Gödel’s second incompleteness theorem is generally considered to show that this particular version of instrumentalism cannot be carried out. Consensus on this question is not complete, however, and variants of Hilbert’s Program have been proposed (in particular, by Detlefsen) which avoid this conclusion. I will discuss an argument based on Gödel’s first incompleteness theorem, which, I argue, is a stronger argument against Hilbert’s Program than the usual argument invoking the second theorem, and which also raises difficult issues about Detlefsen’s instrumentalism.

Proof theory for reasoning with Euler diagrams
Ryo Takemura (Keio University )

Abstract: We introduce a proof-theoretical framework for reasoning with Euler diagrams. We give a translation of an Euler diagrammatic system into a natural deduction system. We discuss some consequences of the translation in terms of Shimojima’s free ride, which is one of the most basic properties of diagrams that is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. We further investigate a notion of normal form of Euler diagrammatic proofs, and show a normalization theorem. We then discuss some consequences of the theorem: an analysis of the structure of normal diagrammatic proofs; a diagrammatic counterpart of the usual subformula property; a characterization of diagrammatic proofs compared with natural deduction proofs.

Reverse Mathematics & Non-Standard Analysis: WHY SOME THEOREMS ARE MORE EQUAL THAN OTHERS
Sam Sanders (Ghent University and Tohoku University )

Abstract: Reverse Mathematics is a program in foundations of mathematics initiated by Friedman ([1,2]) and developed extensively by Simpson ([4]). Its aim is to determine which minimal axioms prove theorems of ordinary mathematics. Nonstandard Analysis plays an important role in this program ([3,6]). We are interested in Reverse Mathematics where equality is replaced by the equality up to infinitesimals from Nonstandard Analysis. We obtain a ‘copy’ of Reverse Mathematics for WKL0 and ACA0 in a weak system of Nonstandard Analysis. Our results also have implications for the Philosophy of Science. In particular, we show how the very nature of Mathematics in Physics implies that real numbers are not needed in Physics.

A GENTLE INTRODUCTION TO LUDICS
Michele Basaldella (Kyoto University )

Abstract: When one is interested in understanding the duality between syntax(proofs) and semantics (models) in logic, a primary obstacle is that proofs are finite and concrete objects, while models are infinite andabstract. Since proofs and models are so different by their nature,they hardly interact together. This lack of interaction between thetwo worlds prevents a deeper analysis of the problem.

Ludics is a research program started by Girard aimed to explain variouslogical and computational phenomena from an interactive point of view. The universe of ludics consists of designs, (possibly) partial andinfinitary proofs in which the logical type-information has been almosterased. In this vast universe, both proofs and models can behomogeneously represented as designs. Moreover, since designs come from proofs, we can make them interact together via normalization (cut-elimination). This induces an orthogonality relation, based on thetermination of the computation of the normal form, which allows toreconstruct the logical types, as bi-orthogonality closed sets of designs.

In this talk we discuss the basic concepts of ludics from a proof-theoretical and computational perspective.




本研究集会は慶應義塾大学「論理学とフォーマルオントロジー」オープンリサーチセンターと慶應義塾大学グローバルCOE「論理と感性の先端的教育研究拠点」 の共催研究集会です。
   問い合わせ先:
     慶應義塾大学「論理学とフォーマルオントロジー」オープンリサーチセンター事務局
     住所: 東京都港区三田2-15-45
     TEL: 03-3453-4511 (内線23847)
     E-Mail: logic[AT]abelard.flet.keio.ac.jp

なお,セミナーの最新の情報は以下のページに掲示されます.
http://abelard.flet.keio.ac.jp/ptp11/


This document was translated from LATEX by HEVEA.