Modal translations in substructural logics
The Gödel-Tarski translation of the intuitionistic predicate logic into S4 by prefixing \(\square\) to all subformulas is sound and faithful. The author proves a similar result for translations of the intuitionistic versions of linear logic, relevance logic and BCK-logic into their classical S4-analogs. The proof uses analysis of cut-free Gentzen-type derivations.
translations of intuitionistic logics into modal logics
analysis of cut-free Gentzen-type derivations
scientific article; zbMATH DE number 92835
scientific article