[logic-ml] Workshop on Logic and Philosophy of Logic, March 19th(Thu)-20th(Fri), 2015

Tue Mar 10 21:54:44 JST 2015

---------------------------------------------------------------------
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 at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20150310/7e1899f3/attachment-0001.html>