Undecidability results on two-variable logics (Q1306795)

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 \(\varepsilon\)-operator. In fact all these extensions of \(L^2\) prove to be undecidable both for satisfiability, and for satisfiability in finite models. Moreover most of them are hard for \(\Sigma^1_1\), the first level of the analytical hierarchy, and thus have a much higher degree of undecidability than first-order logic.