PROOF THEORY AND PHILOSOPHY |
現代論理学、特に証明論から引き出された文脈のなかで、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.
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.
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.
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.
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.