Undecidability results on two-variable logics

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