Burgess, John P.; Gurevich, Yuri The decision problem for linear temporal logic. (English) Zbl 0573.03004 Notre Dame J. Formal Logic 26, 115-128 (1985). The main result of this paper is the decidability of the set of universal monadic second-order sentences true in the structure consisting of the real numbers equipped with the usual order relation. Two proofs are given, the first exploiting a theorem of Rabin, and the second a method of Läuchli and Leonard. There are two corollaries to the proofs: First, for every false univesal monadic second-order sentence about the real order, there exist Borel sets of reals constituting a counterexample. Second, exactly the same universal monadic second-order sentences that are true for the real order are true for any other order that is dense, complete, without endpoints, and satisfies one further universal monadic second-order condition. (Examples are such orders as the ”long-line” and ”Suslin lines”.) Results about universal monadic second-order logic are closely connected with results about ”temporal logic”: This connection is exploited in one of the proofs. Cited in 2 ReviewsCited in 16 Documents MSC: 03B25 Decidability of theories and sets of sentences 03B45 Modal logic (including the logic of norms) 03E15 Descriptive set theory 03C85 Second- and higher-order model theory Keywords:universal monadic second-order sentences; real order; Borel sets of reals; long-line; Suslin lines PDFBibTeX XMLCite \textit{J. P. Burgess} and \textit{Y. Gurevich}, Notre Dame J. Formal Logic 26, 115--128 (1985; Zbl 0573.03004) Full Text: DOI