It is a classical result of Mortimer that
, first-order logic with two variables, is decidable for satisfiability. We show that going beyond
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
-operator.
In fact all these extensions of
prove to be undecidable both for satisfiability, and for satisfiability in finite structures. Moreover most of them are hard
for
, the first level of the analytical hierachy, and thus have a much higher degree of undecidability than first-order logic.
Received: 13 July 1996