Title: Knowing How to Understand Intuitionistic Logic

Speaker: Yanjing Wang (PKU)

Time: 15:10-18:00 Jan 5, 2021

Location: 413 Teaching Building No.2 

Abstract: The goal of the talk is to provide an intuitive and precise understanding of intuitionistic logic and its relatives grounded both mathematically and philosophically. We decode intuitionistic logic as a dynamic epistemic logic of knowing how (to prove) by using the state-of-art tools and ideas from philosophical logic and formal epistemology. The approach is inspired by some scattered but related ideas hidden in the vast literature of math, philosophy, CS, and linguistics about intuitionistic logic in the past 100 years, which echoed Heyting's initial idea about intuitionistic truth. Many important technical results of intuitionistic logic, such as double negation translations and modal embedding, become transparent,  if not trivial. In this approach, BHK interpretation is also connected to Kripke semantics in a precise manner. Some philosophical debates regarding intuitionistic logic can be clarified to some extent. It also paves a way to understanding a class of related non-classical logics as intuitive epistemic logics. I shall conclude with some ongoing work and future directions.