Decidable temporal and sequential relevant logics

摘要

A Gentzen-type sequent calculus STRW is introduced for a new temporal relevant logic TRW, which is obtained from the positive contraction-less relevant logic RW~+ by adding temporal operators. A Gentzen-type sequent calculus SSRW is also introduced for a new sequential relevant logic SRW, which is obtained from RW~+ by adding a sequence modal operator. The SSRW sequence modal operator is regarded as a generalization of the standard next-time temporal operator and can suitably represent sequential information. The cut-elimination and completeness theorems for STRW and SSRW are proved, and STRW and SSRW are shown to be decidable and have relevance principle.