Premium
Temporal Gödel‐Gentzen and Girard translations
Author(s) -
Kamide Norihiro
Publication year - 2013
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.201100083
Subject(s) - sequent , mathematics , intuitionistic logic , embedding , minimal logic , sequent calculus , cut elimination theorem , extension (predicate logic) , calculus (dental) , intermediate logic , discrete mathematics , linear logic , pure mathematics , proof calculus , zeroth order logic , computer science , multimodal logic , artificial intelligence , description logic , mathematical proof , programming language , geometry , medicine , dentistry
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.