Proof-theoretic analysis of negative translations in substructural logics

Hiroakira Ono (Japan Advanced Institute of Science and Technology)

Hiroakira Ono (JAIST) will present "Proof-theoretic analysis of negative translations in substructural logics" on 23 February at 11 in Old Arts 156. 

Abstract: A well-known result by V. Glivenko says that a formula A is provable in classical logic iff the double negation ~ ~ A is provable in intuitionistic logic. In this sense, classical logic can be embedded into intuitionistic logic. More detailed yet elementary proof-theoretic analysis gives us a result which says that classical logic can be embedded into a much more weaker logic (over intuitionistic linear logic). Applying the same idea to classical predicate logic, we will show what will happen for Kuroda translation in the context of substructural predicate logics. Lastly we will propose a new translation, called extended Kuroda translation, and compare it with other negative translations, including Kolmogorov translation.