<div dir="ltr"><div><div class="gmail_signature"><div dir="ltr"><div><span style="font-size:14px">------------------------------<u></u>------------------------------<u></u>---------<br>We apologize if you receive this message more than once.<br>------------------------------<u></u>------------------------------<u></u>---------<br><br>The following Workshop on Logic and Philosophy of Logic is scheduled.<br></span><span style="font-size:14px">次のようなワークショップ「Workshop on Logic and Philosophy of Logic」</span><br style="font-size:14px"><span style="font-size:14px">を予定しております。参加自由です。</span><span style="font-size:14px"><br><br>----<br><br>Workshop on Logic and Philosophy of Logic<br></span><span style="font-size:14px">「論理学・論理哲学ワークショップ」</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Date: March 19th(Thu)-20th(Fri), 2015</span><span style="font-size:14px"><br>日時: 2015年3月19日(Thu)-20日(Fri)<br>Place: Distance Learning Room (B4F), South Building, Mita campus of Keio University.<br></span><span style="font-size:14px">場所: 慶應大学三田キャンパス 南館地下4階 ディスタンスラーニングルーム</span><span style="font-size:14px"><br>(<a href="http://www.keio.ac.jp/en/maps/mita.html" target="_blank">http://www.keio.ac.jp/en/<u></u>maps/mita.html</a>   13番の建物です。/ Building #13 on this map.)<br></span><span style="font-size:14px">URL: </span><a href="http://ctj.keio.ac.jp/news/27" target="_blank" style="font-size:14px">http://ctj.keio.ac.jp/news/27</a><span style="font-size:14px"> (*最新プログラムはこちらでご確認ください)</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">----</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Tentative Program:</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">3/19:</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">13:00-13:10 Opening Remark, Mitsuhiro Okada (Keio University)</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">13:00-13:50 Makoto Fujiwara (Tohoku University, Department of Mathematics): "Constructive provability versus uniform provability in classical computable mathematics"</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">13:50-14:50 Giovanni Sambin (Dipartimento di Matematica Pura e Applicata, Università di Padova): "A single system for a plurality of logics"</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">14:50-15:20 Break</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">15:20-16:10 Gergei Bana (INRIA, France) "Fitting's model construction and computability" (joint work with Mitsuhiro Okada)</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">16:10-17:10 Sandra Laugier (Université Paris 1, Centre de Philosophie Contemporaine de la Sorbonne) "Rule-Following, Practice, and Forms of life"</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">17:10-17:30 Discussion</span><br style="font-size:14px"><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">3/20:</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">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)</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">11:10-12:00 Shunsuke Yatabe (West Japan Railway Company): "Is truth a logical connective?"</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">12:00-13:30 Lunch Break</span><span style="font-size:14px"><br><br>13:30-14:30 Mirja Hartimo (University of Jyväskylä, Department of Social Sciences and Philosophy) "Husserl and mathematics in the 1920s"　<br><br></span><span style="font-size:14px">14:30-14:50 Break</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">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"</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">15:50-16:10 Break</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">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"</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">17:00-17:20 Concluding Discussion</span><span style="font-size:14px"><br><br>------------------------------<u></u>------------------------------<u></u>---------<br><br>Organisers:<br>Ryota Akiyoshi (co-chair)<br>Mitsuhiro Okada (co-chair)<br>Yutaro Sugimoto<br>Yuta Takahashi<br><br></span><span style="font-size:14px">主催: 慶應義塾大学「思考と行動判断」の研究拠点</span><br style="font-size:14px"><span style="font-size:14px">共催: 慶應義塾大学 論理と感性のグローバル研究センター</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">問合せ先:</span><br style="font-size:14px"><span style="font-size:14px">Mita Logic Seminar /「思考と行動判断」の研究拠点 事務局</span><br style="font-size:14px"><a href="mailto:logic@abelard.flet.keio.ac.jp" target="_blank" style="font-size:14px">logic@abelard.flet.keio.ac.jp</a><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">-------------------------</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">ABSTRACTS:</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Makoto Fujiwara "Constructive provability versus uniform provability in classical computable mathematics"</span><span style="font-size:14px"><br><br>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.<br><br></span><span style="font-size:14px">----</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Giovanni Sambin "A single system for a plurality of logics"</span><span style="font-size:14px"><br><br>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.<br><br>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.<br><br></span><span style="font-size:14px">----</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Gergei Bana "Fitting’s model construction and computability" (joint work with Mitsuhiro Okada)</span><span style="font-size:14px"><br><br>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.<br><br></span><span style="font-size:14px">----</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Sandra Laugier "Rule-Following, Practice, and Forms of life"</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">TBA</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">----</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Ukyo Suzuki "The Possibility of Predicative Arithmetic" (可述算術の可能性)</span><span style="font-size:14px"><br><br>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.<br><br></span><span style="font-size:14px">(この発表では、エドワード・ネルソン(1932-2014)</span><u style="font-size:14px"></u><span style="font-size:14px">の</span><span style="font-size:14px">可述算術の興味を、</span><u style="font-size:14px"></u><span style="font-size:14px">非改訂主義的観点から捉えるアイデアを提示す</span><span style="font-size:14px">る。はじめに、</span><u style="font-size:14px"></u><span style="font-size:14px">可述算術という研究プログラムを、</span><u style="font-size:14px"></u><span style="font-size:14px">ネルソン自身の</span><span style="font-size:14px">改訂主義的モチベーションと共に簡単に解説する。</span><u style="font-size:14px"></u><span style="font-size:14px">次に、</span><span style="font-size:14px">可述算術が、ウィトゲンシュタインによって提示された、</span><u style="font-size:14px"></u><span style="font-size:14px">概念形成</span><span style="font-size:14px">としての数学的証明という考え方に、</span><u style="font-size:14px"></u><span style="font-size:14px">形式的モデルを提供するもの</span><span style="font-size:14px">であることを示唆したい。</span><u style="font-size:14px"></u><span style="font-size:14px">この捉え方が正しければ、</span><span style="font-size:14px">ダメットによって提示されたいわゆる「</span><u style="font-size:14px"></u><span style="font-size:14px">推論のパラドクス」</span><span style="font-size:14px">に対して、可述算術は、</span><u style="font-size:14px"></u><span style="font-size:14px">ウィトゲンシュタイン的な解答を与える。</span><span style="font-size:14px">)</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">----</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Shunsuke Yatabe "Is truth a logical connective?"</span><span style="font-size:14px"><br><br>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.<br><br>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.<br><br>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.<br><br></span><span style="font-size:14px">---</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Mirja Hartimo "Husserl and mathematics in the 1920s"</span><span style="font-size:14px"><br><br>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.<br><br></span><span style="font-size:14px">---</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Mathieu Marion "Wittgenstein and Intuitionism: The Law of Excluded Middle and Following a Rule"</span><span style="font-size:14px"><br><br>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.<br>g<br><br>., 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<br><br>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.<br><br></span><span style="font-size:14px">---</span><br style="font-size:14px"><br style="font-size:14px"><span style="font-size:14px">Ryota Akiyoshi "An interpretation of Brouwer’s argument of the bar induction via infinitary proof theory"</span><span style="font-size:14px"><br><br>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.<br><br>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.</span><br></div></div></div></div>
</div>