#### Preview

**Abstract**

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

Go to Oxford Journals » home page

Full text: subscription required

How to subscribe Recommend to my Librarian

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.