Workshop on Logic and Philosophy of Logic
論理学・論理哲学ワークショップ
 2015年3月19日(Thu)20日(Fri)
 March 19th(Thu)20th(Fri), 2015
 慶應大学三田キャンパス 南館地下4階 ディスタンスラーニングルーム (キャンパスマップ *13番の建物です)
 Distance Learning Room (B4F), South Building, Mita campus of Keio University. (Campus Map Building #13 on this map.)
Program (tentative):
March.19  
13:0013:10 

13:1013:50 

13:5014:50 

14:5015:20 Break  
15:2016:10 

16:1017:10 

17:1017:30 Discussion  
March.20th  
10:3011:10 

11:1012:00 

12:0013:30 Lunch Break  
13:3014:30 

14:3014:50 Break  
14:5015:50 

15:5016:10 Break  
16:1017:00 

17:0017:20 Concluding Discussion  
Abstracts:
 Speaker:
 Makoto Fujiwara
 Title:
 "Constructive provability versus uniform provability in classical computable mathematics"
 Abstract:
Socalled intuitionistic analysis EL is twosorted 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 metaperspective) establish the equivalence between constructive provability and classical uniform provability in RCA for a large number of existence theorems.
 Speaker:
 Giovanni Sambin
 Title:
 "A single system for a plurality of logics"
 Abstract:
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 prooftheoretic 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 cutelimination procedure which respects structural rules and thus automatically becomes a cutelimination 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.
 Speaker:
 Gergei Bana (joint work with Mitsuhiro Okada)
 Title:
 "Fitting’s model construction and computability"
 Abstract:
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.
 Speaker:
 Sandra Laugier
 Title:
 "RuleFollowing, Practice, and Forms of life"
 Abstract:
TBA
 Speaker:
 Ukyo Suzuki
 Title:
 "The Possibility of Predicative Arithmetic" (可述算術の可能性)
 Abstract:
In this talk, I will present an idea to find a nonrevisionistic 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 conceptformation. If my suggestion is correct, Predicative Arithmetic can give a Wittgensteinian answer to the socalled “paradox of inference” presented by Dummett. (この発表では、エドワード・ネルソン(19322014)の可述算術の興味を、非改訂主義的観点から捉えるアイデアを提示する。はじめに、可述算術という研究プログラムを、ネルソン自身の改訂主義的モチベーションと共に簡単に解説する。次に、可述算術が、ウィトゲンシュタインによって提示された、概念形成としての数学的証明という考え方に、形式的モデルを提供するものであることを示唆したい。この捉え方が正しければ、ダメットによって提示されたいわゆる「推論のパラドクス」に対して、可述算術は、ウィトゲンシュタイン的な解答を与える。)
 Speaker:
 Shunsuke Yatabe
 Title:
 "Is truth a logical connective?"
 Abstract:
Truth theories like the FriedmanSheard's truth theory ({\bf FS}) have two rules, Tin rule and Tout 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 infinitelength. 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.
 Speaker:
 Mirja Hartimo
 Title:
 "Husserl and mathematics in the 1920s"
 Abstract:
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.
 Speaker:
 Mathieu Marion
 Title:
 "Wittgenstein and Intuitionism: The Law of Excluded Middle and Following a Rule"
 Abstract:
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 quasiuniversally 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 LogicoPhilosophicus, where a calculus of numbertheoretic equations is presented: given that these are Scheinsätze and that logic applies to propositions, that calculus is meant to be logicfree. (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. 133134. We have here premises of the notorious ‘rulefollowing’ argument of PI §§ 143242. (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 ‘rulefollowing’ 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.
 Speaker:
 Ryota Akiyoshi
 Title:
 "An interpretation of Brouwer’s argument of the bar induction via infinitary proof theory"
 Abstract:
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 BHKinterpretation 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 Omegarule. 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 Omegarule 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 wellmotivated.
共催：慶應義塾大学「論理と感性」のグローバルリサーチセンター
公開日時: March 10, 2015 11:56