There is another point that I don't get. The page says: "The set of firstorder logical validities in a signature with equality and one unary function" is decidable. But isn't any theory with an nary function logically equivalent to a theory with an n+1ary relation? For example, take some simple function like the zero function. f(n) = 0 is logically equivalent to R(n, 0). Functions are convenient, but they can be dispensed with. If I am correct, then FOL with identity and a unary function is equivalent to FOL with identity and a dyadic relation. But the dyadic predicate calculus is not decidable. What gives?
