# TFAP

## Tokyo Forum For Analytic Philosophy

### Program

^{}Oct 2017

#### Informal Logic and the Logic of Provability

**Speaker:** Hidenori Kurakawa **From:** Kanazawa University **URL:** https://ridb.kanazawa-u.ac.jp/public/detail_en.php?id=4634&page=2&org1_cd=585000
**Abstract:** It is often stated that S4 modal logic is a logic whose necessity operator expresses a certain notion of provability. However, it is also well-known that the necessity operator in S4 cannot be interpreted as the notion of formal provability in a fixed formal system of arithmetic such as Peano Arithmetic (PA) due to Godel's incompleteness theorem. As a result, the necessity operator of S4 is usually interpreted as "informal provability." Finding out a way of talking about the necessity operator of S4 that is compatible with PA turned out to be difficult. In order to understand better the relationship between S4 and PA, Sergei Artemov introduced the Logic of Proofs (LP) around 15 years ago. LP is an "explicit" modal logic in which we have formulas with proof-terms (of form t:A, interpreted as "t is a proof of A") instead of formulas with the necessity operator. In particular, due to a theorem called "the realization theorem," LP can make explicit those structures of "proofs" which are implicit in the necessity operator of S4. Roughly, this theorem establishes the fact the structure of a S4 proof and that of a LP are essentially the same. Nevertheless, one of the outstanding features of LP is that, unlike S4, LP has a sound and complete arithmetic interpretation with respect to PA. Moreover, Artemov argues that via the Godel translation from intuitionistic propositional logic (IPC) into S4, LP establishes a precise connection between IPC and PA. Combining these results, he argues that, at least to some extent, we can give a formal account of the intended but informal semantics for intuitionistic logic that is known as Brouwer-Heyting-Kolmogorov (BHK) interpretation, which gives an interpretation of intuitionistic logical constants in terms of "constructive proofs."
In this talk, we revisit LP and give some philosophical reflections on these results for LP from the viewpoint of "informal provability." Our discussions will be based on conceptual analyses of both the notion of "informal provability" and that of "constructive proofs." We try to give at least a partial answer to a general question, "in what sense does LP give a formal account of BHK interpretation?" In particular, we do this by addressing the following questions. i) What is informal provability? ii) In what sense is S4 (LP) a logic of informal provability (proofs), respectively? iii) What role does the Godel translation play in Artemov's account of BHK interpretation? iv) Which aspects of constructive proofs does LP give an account of? We also give a survey of those technical results for LP which are pertinent to our philosophical discussions.

^{}Oct 2017

#### TBA

**Speaker:** Takuya Niikawa **From:** Chiba University & Fuji Women's University **URL:** https://chiba-u.academia.edu/TakuyaNiikawa
**Abstract:** TBA

^{}Nov 2017

#### TBA

**Speaker:** Yoshiyuki Hayashi **From:** University of Tokyo **URL:** http://researchmap.jp/yoshiyuki_hayashi/
**Abstract:** TBA

^{}Nov 2017

#### TBA

**Speaker:** Rob Sinclair **From:** Soka University **URL:** http://fila.soka.ac.jp/en/faculty_sinclair.html
**Abstract:** TBA

^{}Dec 2017

#### TBA

**Speaker:** Shuhei Shimamura **From:** Nihon University **URL:** http://researchmap.jp/sshimamura/?lang=english
**Abstract:** TBA

^{}Dec 2017

#### TBA

**Speaker:** Akira Inoue **From:** University of Tokyo **URL:** http://u-tokyo.academia.edu/AkiraInoue
**Abstract:** TBA