The purpose of this mini-workshop is to discuss recent developments and new ideas about non-classical logic, in the occasion of Dr. Tadeusz Litak's visit to Sapporo. 

24th March 2023, 13:00~15:30

24th March 2023

• 13:00-13:10 Opening

• 13:10-13:50 Katsuhiko Sano (Hokkaido University)

 Axiomatizing a simple logic of the hide and seek game

• 13:50-14:00 Break

• 14:00-14:40 Masanobu Toyooka (Hokkaido University) 

About coexistence of intuitionistic implication and classical negation in the level of first-order logic

• 14:40-14:50 Break

• 14:50-15:30 Tadeusz Litak (Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU) )

A quick overview of constructive strict implication

• 15:30 Closing 

Instead of banquet, just after the workshop, we plan to go to a cafe (Cafe Polus ぽらす) at the university museum for our further discussions. 

• Katsuhiko Sano:  Axiomatizing a simple logic of the hide and seek game

This talk provides a semantically complete axiomatization of a hybridization of a simple modal logic of the hide and seek game by Li et al. (2021). To describe the winning condition of the seeker of the game the logic has an equality constant, which is similar to the diagonal constant introduced in the product of modal logics by Kurucz (2009). While the original simple modal logic of the hide and seek game was shown to be undecidable in Li et al. (2021), it is still open that the logic has a semantically complete axiomatization. In this talk, we show that a hybridization (a machinery of hybrid logic, in particular, that for the product of modal logic, cf. Sano (2010)) provides an answer to the open question, provided the syntax is expanded with nominals and satisfaction operators. This is joint work with Dazhu Li (Chinese Academy of Sciences) and Fenrong Liu (Tsinghua).

• Masanobu Toyooka: About coexistence of intuitionistic implication and classical negation in the level of first-order logic

This presentation compares two logics where intuitionistic implication and classical negation coexist in the first-order level. The first one is FOC+J, which is a first-order expansion of the logic called C+J, proposed by Humberstone (1979) and del Cerro & Herzig (1996). This expansion was already proposed by Lucio. The second one is CD~, which is a first-order expansion of the logic called IPC~, proposed by De (2013) and De & Omori (2014). This logic is newly introduced in this presentation. This compares the two logics in terms of various properties.

• Tadeusz Litak: Lewis meets Brouwer: A quick overview of constructive strict implication

C. I. Lewis invented modern modal logic as the theory of  "strict implication". Nevertheless, over the classical propositional calculus one can as well work with unary box, which became the standard modal connective. Intuitionistically, however, strict implication has greater expressive power. I will illustrate its various appearances, including schematic logics of extensions of Heyting Arithmetic,  the Curry-Howard correspondence for "arrows" in functional programming or (still underdeveloped) Intuitionistic Epistemic Logic of Entailment. Interestingly, the minimal system sound for all these interpretations requires non-Kripkean semantics. Time permitting, I may briefly discuss technical results for important extensions of the basic system (the fmp, completeness, correspondence, definability of fixpoints, uniform interpolation...) obtained jointly with Albert Visser (Utrecht) and Jim de Groot and Dirk Pattinson (ANU), possibly also some work in progress with Igor Sedlar and the Prague group.

This mini-workshop is supported by JSPS KAKENHI Grant Number JP19K12113.

Katsuhiko Sano (Hokkaido University)  ("katsuhiko.sano" plus "@" plus "gmail.com") & Masanobu Toyooka (Hokkaido University)