Tokyo Forum For Analytic Philosophy

Program

Friday 20 Oct 2017
Hidenori Kurakawa

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.

 
 
Friday 27 Oct 2017
Takuya Niikawa

TBA

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

 
 
Monday 20 Nov 2017
Yoshiyuki Hayashi

TBA

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

 
 
Wednesday 29 Nov 2017
Rob Sinclair

TBA

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

 
 
Monday 4 Dec 2017
Shuhei Shimamura

TBA

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

 
 
Monday 11 Dec 2017
Akira Inoue

TBA

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