第20回CAPEレクチャー:A Frontier of Non-Classical Logic

第20回CAPEレクチャー:A Frontier of Non-Classical Logic
日時:2013年7月19日(金)10:30-14:30
場所:京都大学文学研究科 地下小会議室
http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm
(8番の建物です)
タイムテーブル:
10:30 – 12:00
“Alternative Semantics for Visser’s Basic Propositional Logic”
Katsuhiko Sano (JAIST)

abstract
Visser (1981)’s Basic Propositional Logic (BPL) has the same syntax
with classical and intuitionistic logics and it is complete over the
class of transitive Kripke models with persistent valuations. In this
sense, BPL can be regarded as a `sub’-intuitionistic logic.
Especially, BPL can block a derivation of A -> B from A -> (A -> B),
which is used in a derivation of Curry’s paradox. Visser showed that
Goedel-Mckinsey-Tarski translation can embed BPL and an extension of
BPL into modal logics K4 and GL (provability logic by Loeb),
respectively. This talk proposes a generalization of
Goedel-Mckinsey-Tarski translation and establish that we can embed the
logic of weakly transitive Kripke frames (wK4), studied by Esakia
(2001), into BPL. This translation result leads us to propose a
topological semantics for BPL with completeness result. This talk
first gives a general introduction to BPL and then explains the main
contribution above. This is an on-going joint work with Minghui Ma
(Southwest University).

13:00 – 14:30
“Substructural logic of proofs and self-referentiality”
Hidenori Kurokawa (Kobe University)
and Hirohiko Kushida (CUNY)

abstract
In this talk, we first give a general introduction to Artemov’s logic
of proofs. We present its basic ideas, motivations, and some
fundamental results. Then we introduce substructural variants of logic
of proofs. We present a few things. First, we introduce a bimodal
logic that has both the exponential operator in linear logic and an S4
modal operator which does not bring in any structural feature. Both
Girard’s embedding and Godel’s modal embedding (not the double
negation translation) are used in order to directly connect
intuitionistic substructural logics and substructural logics with the
involutive negation. Second, we formulate substructural logic of
proofs, which is an explicit counterpart of the foregoing bimodal
substructural logics, and show that the substructural logic of proofs
can realize the bimodal substructural logic, following the idea of
(Artemov 2001). Third, adopting the idea of (Yu 2010), we also show
that the contraction-free, multiplicative S4-fragment of the bimodal
substructural logic is realizable without appealing to a so-called
“self-referential constant specification.”