I always thought that first order logic with identity was undecidable if it had either a 2-place relation or a 2-place function. Wikipedia seems to confirm what I'd thought: "The set of logical validities in any first-order signature with equality and either: a relation symbol of arity no less than 2, or two unary function symbols, or one function symbol of arity no less than 2, established by Trakhtenbrot in 1953." http://en.wikipedia.org/wiki/Decidability_(logic) But from the same page it lists as decidable: "The first-order theory of the integers in the signature with equality and addition, also called Presburger arithmetic. The completeness was established by Mojżesz Presburger in 1929." I was aware that Presburger arithmetic is decidable, but I'd never thought about how this relates to the undecidability of first order logic with at least a binary function. Addition is a two-place function. Can anyone explain how Presburger arithmetic can be decidable, since it contains first order logic, identity, and a two-place function? I'm not exactly asking for a proof of the decidability of Presburger arithmetic. What I'm asking is how it can be consistent with the requirement that FOL + identity and a binary function is undecidable.