Decidability of Presburger arithmetic and FOL

[Jeroslaw]

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.

 

[Jeroslaw]

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?

 

[Dragonfall]

Can you cite where you learned that FOL + binary function is undecidable?

 

[Hurkyl]

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."

The wikipedia quote looks like it's referring specifically to the first-order theory with that signature and no axioms.

 

[Jeroslaw]

The wikipedia quote looks like it's referring specifically to the first-order theory with that signature and no axioms.

Let *PA* represent the conjunction of the non-logical axioms of Presburger arithmetic. So, what you're saying is that we have a way of determining for an arbitrary sentence S whether *PA* l- S. However, we can't determine for an arbitrary S whether or not l- S in first order logic with a binary function and no non-logical axioms.

I have seen proofs of Church's theorem which take the following route to undecidability: first they show that some arithmetical theory is undecidable(usually Robinson arithmetic). Then they say that if first order logic were decidable, it could determine whether or not the conjunction of Robinson arithmetic's non-logical axioms implies an arbitrary S. But this is impossible because Q is undecidable, so FOL cannot be decidable either. If there is one undecidable statement, the logic or theory is undecidable.

Then if you have a decidable theory such as Presburger, FOL should be able to decide whether or not the conjunction of its axioms implies an arbitrary S. That is, whether or not we have l- *PA* -> S. Does this mean that the logic must be decidable, even though it has a binary function? It would seem not, since although it can decide whether or not PA's axioms imply S, it might not be able to decide whether or not S is a theorem of the logic. What it amounts to is that statements of the form (*PA* -> S) are decidable, but that doesn't mean that all statements in the language of PA are decidable.

I'll have to revisit this when I'm not so tired. Are we on the same page?

By the way, is it true that functions can be replaced by logically equivalent relations?

 

[Hurkyl]

What it amounts to is that statements of the form (*PA* -> S) are decidable, but that doesn't mean that all statements in the language of PA are decidable.

It does mean that all statements in the language of PA are decidable in PA. Recall that a statement S is a theorem in the theory Peano arithmetic if and only if (PA -> S) is a theorem of first-order logic.

 

[Jeroslaw]

It does mean that all statements in the language of PA are decidable in PA. Recall that a statement S is a theorem in the theory Peano arithmetic if and only if (PA -> S) is a theorem of first-order logic.

When I said 'PA' I was referring to Presburger Arithmetic. As for the other point, what I meant is that an arbitrary sentence formulated in the language of Presburger Arithmetic is not decidable in first order logic with no assumptions, although it is decidable whether or not it follows from the axioms of Presburger Arithmetic(PA l- S is decidable, l- PA -> S is decidable, l- S is not decidable). We're saying the same thing, wouldn't you say?

 

[TXLogic]

It does mean that all statements in the language of PA are decidable in PA. Recall that a statement S is a theorem in the theory Peano arithmetic if and only if (PA -> S) is a theorem of first-order logic.

That isn't so. PA isn't finitely axiomatizable, so there is no such sentence as (PA -> S).

 

[JSuarez]

Can anyone explain how Presburger arithmetic can be decidable, since it contains first order logic, identity, and a two-place function?

Suppose that $\alpha$ is a sentence of FOL with equality and a binary function and "feed" it to the decision algorithm of Presburger Arithmetic (PrA) (which is called quantifier elimination); if the answer is "yes", then you may be sure that $\alpha$ is a theorem of PrA, but not a logically valid sentence: don't forget that you can prove infinitely many theorems of PrA that aren't logically valid. This shows that you cannot use the decidability of PrA to identify logically valid expressions (you may use to prove that a sentence is not logically valid, though).

But the dyadic predicate calculus is not decidable. What gives?

When you eliminate a binary function symbol and replace it with a binary relation one, then the behaviour of the latter is restricted (not all relations are functions); therefore, the decidability of the binary function language doesn't contradict the undecidability of the language with an arbitrary binary relation.

 

[Hurkyl]

That isn't so. PA isn't finitely axiomatizable, so there is no such sentence as (PA -> S).

This thread is over three years old, but anyways... In a context where this needs correction, it is clear:

... if and only if there is a subset T of the axioms of PA such that T -> S is a tautology​