Undecidability results on two-variable logics

Archive for Mathematical Logic 38 (4-5):313-354 (1999)
  Copy   BIBTEX

Abstract

It is a classical result of Mortimer that $L^2$ , first-order logic with two variables, is decidable for satisfiability. We show that going beyond $L^2$ by adding any one of the following leads to an undecidable logic:– very weak forms of recursion, viz.¶(i) transitive closure operations¶(ii) (restricted) monadic fixed-point operations¶– weak access to cardinalities, through the Härtig (or equicardinality) quantifier¶– a choice construct known as Hilbert's $\epsilon$ -operator.In fact all these extensions of $L^2$ prove to be undecidable both for satisfiability, and for satisfiability in finite structures. Moreover most of them are hard for $\Sigma^1_1$ , the first level of the analytical hierachy, and thus have a much higher degree of undecidability than first-order logic

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Two variable first-order logic over ordered domains.Martin Otto - 2001 - Journal of Symbolic Logic 66 (2):685-702.
Deciding regular grammar logics with converse through first-order logic.Stéphane Demri & Hans De Nivelle - 2005 - Journal of Logic, Language and Information 14 (3):289-329.
Decidable fragments of first-order modal logics.Frank Wolter & Michael Zakharyaschev - 2001 - Journal of Symbolic Logic 66 (3):1415-1438.
On the restraining power of guards.Erich Grädel - 1999 - Journal of Symbolic Logic 64 (4):1719-1742.
An Event-Based Fragment of First-Order Logic over Intervals.Savas Konur - 2011 - Journal of Logic, Language and Information 20 (1):49-68.
The Price of Universality.Edith Hemaspaandra - 1996 - Notre Dame Journal of Formal Logic 37 (2):174-203.
More on The Decidability of Mereological Theories.Hsing-Chien Tsai - 2011 - Logic and Logical Philosophy 20 (3):251-265.
Complexity Results of STIT Fragments.François Schwarzentruber - 2012 - Studia Logica 100 (5):1001-1045.

Analytics

Added to PP
2013-11-23

Downloads
24 (#563,255)

6 months
1 (#1,042,085)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

On the restraining power of guards.Erich Grädel - 1999 - Journal of Symbolic Logic 64 (4):1719-1742.
Two variable first-order logic over ordered domains.Martin Otto - 2001 - Journal of Symbolic Logic 66 (2):685-702.
Syllogistic Logic with Comparative Adjectives.Lawrence S. Moss - 2011 - Journal of Logic, Language and Information 20 (3):397-417.

View all 9 citations / Add more citations

References found in this work

Fixed-point extensions of first-order logic.Yuri Gurevich & Saharon Shelah - 1986 - Annals of Pure and Applied Logic 32:265-280.
The decision problem for standard classes.Yuri Gurevich - 1976 - Journal of Symbolic Logic 41 (2):460-464.
Entscheidungsproblem Reduced to the ∀∃∀ Case.A. S. Kahr, Edward F. Moore & Hao Wang - 1962 - Journal of Symbolic Logic 27 (2):225-225.

Add more references