Undecidability Results on Two-Variable Logics

摘要

It is a classical result of Mortimer's that L~2, first-order logic with two variables, is decidable for satisfiability (whereas L~3 is undecidable). We show that going beyond L~2 by adding any one of the following leads to an undecidable logic