View Single Post
Mar12-08, 03:35 AM
P: 8
There is another point that I don't get. The page says: "The set of first-order logical validities in a signature with equality and one unary function" is decidable. But isn't any theory with an n-ary function logically equivalent to a theory with an n+1-ary 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?