The relationship among first-order monadic omega-logic (MOL), propositional (until-free) linear-time temporal logic (LTL), propositional generalized definitional reflection logic (GDRL) and propositional infinitary logic (IL) is clarified via embedding theorems. A theorem for embedding a Gentzen-type sequent calculus MO[math] for MOL into a Gentzen-type sequent calculus LT[math] for LTL is proved. The cut-elimination theorem for MO[math] is proved using this embedding theorem. MOL is also shown to be decidable through the use of this embedding theorem. Theorems for embedding LT[math] into MO[math] and MO[math] into a Gentzen-type sequent calculus LK[math] for IL are also proved. Moreover, a theorem for embedding MO[math] into a Gentzen-type sequent calculus GD[math] for GDRL and a theorem for embedding LT[math] into GD[math] are proved.
Keywords: First-order monadic omega-logic; linear-time temporal logic; generalized definitional reflection logic; infinitary logic; embedding theorem; cut-elimination theorem
Journal Article. 10086 words. Illustrated.
Subjects: Computing ; Logic
Full text: subscription required