Relating first-order monadic omega-logic, propositional linear-time temporal logic, propositional generalized definitional reflection logic and propositional infinitary logic

摘要

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. Atheorem for embedding a Gentzen-type sequent calculusMO. forMOLinto a Gentzen-type sequent calculus LT. for LTL is proved. The cut-elimination theorem for MO. is proved using this embedding theorem. MOL is also shown to be decidable through the use of this embedding theorem. Theorems for embedding LT. into MO. and MO. into a Gentzen-type sequent calculus LK. for IL are also proved. Moreover, a theorem for embedding MO. into a Gentzen-type sequent calculus GD. for GDRL and a theorem for embedding LT. into GD. are proved.