Abstract

A theorem for embedding a first-order linear- time temporal logic LTL into its intuitionistic counterpart ILTL is proved using Baratella-Masini's temporal extension of the Gödel-Gentzen negative translation of classical logic into intuitionistic logic. A substructural counterpart LLTL of ILTL is introduced, and a theorem for embedding ILTL into LLTL is proved using a temporal extension of the Girard translation of intuitionistic logic into intuitionistic linear logic. These embedding theorems are proved syntactically based on Gentzen-type sequent calculi.