--------------------------------------------------------------------- We apologize if you receive this message more than once. ---------------------------------------------------------------------
The following Workshop on Logic and Philosophy of Logic is scheduled. 次のようなワークショップ「Workshop on Logic and Philosophy of Logic」 を予定しております。参加自由です。
----
Workshop on Logic and Philosophy of Logic 「論理学・論理哲学ワークショップ」
Date: March 19th(Thu)-20th(Fri), 2015 日時: 2015年3月19日(Thu)-20日(Fri) Place: Distance Learning Room (B4F), South Building, Mita campus of Keio University. 場所: 慶應大学三田キャンパス 南館地下4階 ディスタンスラーニングルーム (http://www.keio.ac.jp/en/maps/mita.html 13番の建物です。/ Building #13 on this map.) URL: http://ctj.keio.ac.jp/news/27 (*最新プログラムはこちらでご確認ください)
----
Tentative Program:
3/19:
13:00-13:10 Opening Remark, Mitsuhiro Okada (Keio University)
13:00-13:50 Makoto Fujiwara (Tohoku University, Department of Mathematics): "Constructive provability versus uniform provability in classical computable mathematics"
13:50-14:50 Giovanni Sambin (Dipartimento di Matematica Pura e Applicata, Università di Padova): "A single system for a plurality of logics"
14:50-15:20 Break
15:20-16:10 Gergei Bana (INRIA, France) "Fitting's model construction and computability" (joint work with Mitsuhiro Okada)
16:10-17:10 Sandra Laugier (Université Paris 1, Centre de Philosophie Contemporaine de la Sorbonne) "Rule-Following, Practice, and Forms of life"
17:10-17:30 Discussion
3/20:
10:30-11:10 Ukyo Suzuki (The University of Tokyo, Department of History and Philosophy of Science): "The Possibility of Predicative Arithmetic" (Talk in Japanese, possibly with English slides)
11:10-12:00 Shunsuke Yatabe (West Japan Railway Company): "Is truth a logical connective?"
12:00-13:30 Lunch Break
13:30-14:30 Mirja Hartimo (University of Jyväskylä, Department of Social Sciences and Philosophy) "Husserl and mathematics in the 1920s"
14:30-14:50 Break
14:50-15:50 Mathieu Marion (Université du Québec à Montréal, Philosophie Department) "Wittgenstein and Intuitionism: The Law of Excluded Middle and Following a Rule"
15:50-16:10 Break
16:10-17:00 Ryota Akiyoshi (Kyoto University, Department of Philosophy) "An interpretation of Brouwer’s argument of the bar induction via infinitary proof theory"
17:00-17:20 Concluding Discussion
---------------------------------------------------------------------
Organisers: Ryota Akiyoshi (co-chair) Mitsuhiro Okada (co-chair) Yutaro Sugimoto Yuta Takahashi
主催: 慶應義塾大学「思考と行動判断」の研究拠点 共催: 慶應義塾大学 論理と感性のグローバル研究センター
問合せ先: Mita Logic Seminar /「思考と行動判断」の研究拠点 事務局 logic@abelard.flet.keio.ac.jp
-------------------------
ABSTRACTS:
Makoto Fujiwara "Constructive provability versus uniform provability in classical computable mathematics"
So-called intuitionistic analysis EL is two-sorted intuitionistic arithmetic, which serves as system to formalize constructive mathematics. In this talk, we show that for any existence theorem T of some syntactical form, T is provable in EL if and only of T is uniformly provable in classical variant RCA of EL. From a philosophical point of view, it might be remarkable that all of our proofs are constructive, namely, they are just explicit syntactic translations. Thus we constructively (from a meta-perspective) establish the equivalence between constructive provability and classical uniform provability in RCA for a large number of existence theorems.
----
Giovanni Sambin "A single system for a plurality of logics"
We propose a single, unified formulation for a wide variety of logics. This is achieved thorugh a sequent calculus UB for classical logic which uses a third structural sign, besides turnstile and comma, to denote active formulas in a context. Then, besides weakening and contraction, structural rules of UB include also some rules for the management of active formulas. All most common logics (classical, intuitionistic, paraconsistent, substructural, both in their intuitionistic and classical version) become literally (equivalent to) subsystems of UB. In other words, our previous approach showing that many logics could be seen as extensions of our basic logic B (JSL 2000), is now fully formal and internalized.
Inference rules for all logical constants in UB are justified through the principle of reflection.This offers a single proof-theoretic semantics for all logical constants in all logics and confirms beyond doubts Dosen's principle saying that a logic is only determined by structural rules.A proof in one of the above logics is just a proof in UB which does not use some of the structural rules. We produce a cut-elimination procedure which respects structural rules and thus automatically becomes a cut-elimination procedure for all logics expressible as subsystems of UB.One benefit is that one can concentrate efforts on UB to improve both understanding and computational efficiency for a wide variety of logics.
----
Gergei Bana "Fitting’s model construction and computability" (joint work with Mitsuhiro Okada)
We review Fitting’s embedding of classical logic into S4, that is, Fitting’s possible world semantics for classical logic.This is closely related to Cohen's forcing.Then we show how this construction naturally emerges when trying to formalize what a (malicious) agent can possibly computeor cannot compute from what is available to the agent as input.Finally, we illustrate how this construction helps us to carry out security proofs for cryptographic prot.
----
Sandra Laugier "Rule-Following, Practice, and Forms of life"
TBA
----
Ukyo Suzuki "The Possibility of Predicative Arithmetic" (可述算術の可能性)
In this talk, I will present an idea to find a non-revisionistic kind of interest in Edward Nelson’s Predicative Arithmetic. First, I’ll briefly summarize Predicative Arithmetic as a research program with Nelson’s own revisionistic motivation. Next, I’ll suggest Predicative Arithmetic can provide a formal model for Wittgenstein’s conception of mathematical proof as concept-formation. If my suggestion is correct, Predicative Arithmetic can give a Wittgensteinian answer to the so-called “paradox of inference” presented by Dummett.
(この発表では、エドワード・ネルソン(1932-2014)の可述算術の興味を、非改訂主義的観点から捉えるアイデアを提示する。はじめに、 可述算術という研究プログラムを、ネルソン自身の改訂主義的モチベーションと共に簡単に解説する。次に、可述算術が、ウィトゲンシュタインによって提示された、 概念形成としての数学的証明という考え方に、形式的モデルを提供するものであることを示唆したい。この捉え方が正しければ、ダメットによって提示されたいわゆる「 推論のパラドクス」に対して、可述算術は、ウィトゲンシュタイン的な解答を与える。)
----
Shunsuke Yatabe "Is truth a logical connective?"
Truth theories like the Friedman-Sheard's truth theory ({\bf FS}) have two rules, T-in rule and T-out rule, about introduction and elimination of the truth predicate. They look like the introduction rule and the elimination rule of a logical connective. From the proof theoretic semantics viewpoint, one might think that the truth predicate is a logical connective which is governed by these two rules.
From this proof theoretic semantics viewpoint, the nature of truth is like
deflationist's nature of truth. Additionally one of the most important things is that the truth predicate does not disturb the traceability of the argument from the premises to a conclusion. However, a crucial problem has been known: any criteria to be a logical connective, known as a ``harmony" of the introduction rule and the elimination rule, are not satisfied because of the $\omega$-inconsistency of FS. Such $\omega$-inconsistency is caused by the fact that the truth predicate enables us to define paradoxical formulae of seemingly infinite-length. These formulae can be regarded as coinductive objects in terms of computer science. The reason of the failure of the harmony is that these criteria are defined not for coinductively defined paradoxical formulae but for inductively defined formulae.
In this talk, we examine how we can extend the criteria for harmony for coinductive formulae in terms of the inversion principle of proftheoretic semantics and corecursive functions in coinductive datatypes.
---
Mirja Hartimo "Husserl and mathematics in the 1920s"
The paper contextualizes Husserl’s writings on mathematics in the 1920s. It offers a look to Husserl’s library and in particular to the books on mathematics he owned and were published after 1917 but before 1929. Some of these books have reading marks showing that Husserl studied them. Four of them have been studied particularly carefully: Hilbert’s 1922 Neubegründung der Mathematik, Weyl’s article ”Die heutige Erkenntnislage in der Mathematik”(1925) and the book Philosophie der Mathematik und Naturwissenschaft (1926). The presentation will discuss the nature of Husserl’s reading marks on these items and then show how these influences can be seen in Husserl’s Formal and Transcendental Logic.
---
Mathieu Marion "Wittgenstein and Intuitionism: The Law of Excluded Middle and Following a Rule"
Wittgenstein attended a lecture by Brouwer in Vienna, in March 1928. Witness accounts by Herbert Feigl and Karl Menger and even Brouwer’s own testimony point to his interest, but there are few comments on typically intuitionistic topics, such as the critique of the unrestricted application of the Law of Excluded Middle, and the impact of intuitionism on his philosophy remains a controversial topic – nowadays, the opinion that it had none is quasi-universally accepted. In this paper, I shall begin by an overview of Wittgenstein’s relation to intuitionism, and then focus on two important topics, the Law of Excluded Middle and ‘following a rule’. On the first, I shall adduce evidence that he agreed with Brouwer’s reasoning, with his ‘weak counterexample’ using the decimal expansion of p (WVC, p. 71, AWL, p. 107 and M, p. 303). But Wittgenstein disagreed with Brouwer’s claim that the Law of Excluded Middle did not apply only for the ‘mathematics of the infinite’ (e. g
., PR § 73 or PG, p. 458); he believed that it does not apply even for elementary number theoretic equations. I shall argue that Wittgenstein’s position can only be understood in terms of the views laid out in the Tractatus Logico-Philosophicus, where a calculus of number-theoretic equations is presented: given that these are Scheinsätze and that logic applies to propositions, that calculus is meant to be logic-free. (This standpoint was further developed in the early 1930s, and led him, for example, to introduce a rule of uniqueness of a function defined by recursion, to do without mathematical induction.) On the second topic, Wittgenstein arrived at the following view of intuitionism in 1929: “each number has its individual properties […] Thus we never get away from the endlessly many individualities” (MS 106, p. 282). (This may not be an appropriate understanding of Brouwer’s views, but I shall leave this question aside.) But this raises a difficulty for the notion of a
general rule and its application, since one “must recognize each time afresh that this rule may be applied […] No act of foresight can absolve me from this act of insight (Einsicht)” (PR, p. 171). See also Ambrose’s lectures notes, AWL, p. 133-134. We have here premises of the notorious ‘rule-following’ argument of PI §§ 143-242. (See, e.g., § 186 and LFM, p. 237 for a late critique of intuitionism along that line.) I shall end the paper by showing thus how the ‘rule-following’ argument embodies a critique of intuitionism, helping myself to recently published remarks by Waismann in his Oxford lectures on causality, and the current debate in analytic philosophy on ‘blind rule following’ sparks by paper by Paul Boghossian and Crispin Wright.
---
Ryota Akiyoshi "An interpretation of Brouwer’s argument of the bar induction via infinitary proof theory"
In a series of papers, Brouwer had developed intuitionistic analysis based on his concept of ``set”. In particular, he derived a key theorem called the fan theorem from another strong theorem called ``the bar induction”. Brouwer gave his argument to justify the bar induction in 1927, which is of great philosophical importance because it was one important source of the BHK-interpretation But the argument essentially depends on the assumption on the form of canonical proofs, so it has been considered as obscure or at least not evident.
In this talk, we sketch an approach to understanding Brouwer’s argument via a tool in infinitary proof theory called the Omega-rule. This tool was introduced by Buchholz for ordinal analysis of impredicative theories. After explaining a historical background of the bar induction and basic notions in intuitionistic analysis, we introduce a version of the Omega-rule to analyze the bar induction and sketch how to embed the bar induction by it. By inspecting the embedding argument, we analyze the role of Brouwer’s assumption and conclude that his argument is mathematically well-motivated.