Journal Article

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

Norihiro Kamide

in Journal of Logic and Computation

Volume 27, issue 7, pages 2271-2301
Published in print October 2017 | ISSN: 0955-792X
Published online February 2017 | e-ISSN: 1465-363X | DOI: http://dx.doi.org/10.1093/logcom/exx006
Relating first-order monadic omega-logic, propositional linear-time temporal logic, propositional generalized definitional reflection logic and propositional infinitary logic

Show Summary Details

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

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.