Presburger Arithmetic - MathOverflow

Presburger Arithmetic

2009-12-27T06:31:26Z

Presburger arithmetic apparently proves its own consistency. Does anyone have a reference to an exposition of this? It's not clear to me how to encode the statement "Presburger arithmetic is consistent" in Presburger arithmetic.

In Peano arithmetic this is possible since recursive functions are representable, so a recursive method of assigning Godel numbers to formulas and proofs means that Peano arithmetic can represent its own provability relation (of course, showing all that requires a lot of work). In particular, we can write a Peano arithmetic sentence which says "there is no natural number which encodes a proof of $\bot$".

On the other hand, Presburger arithmetic can't represent all recursive functions. It can't even represent all the primitive recursive ones, so this same trick doesn't work. If it did, the first incompleteness theorem would apply.

Answer by Jeremy Shipley for Presburger Arithmetic

2009-12-27T18:42:21Z

In your question you say Presburger Arithmetic "proves its own consistency". Really? It's provably consistent, as the wikipedia article notes, but isn't the proof done in a metalanguage? Unfortunately I'm at home for the holiday and don't have references handy, but I'd suggest looking at Peter Smith's "An Introduction to Godel's Theorems" for starters to get clear on this stuff: http://books.google.com/books?id=eK4GmFovS1UC&dq=an+introduction+to+godel%27s+theorems&client=firefox-a&cd=1

I really like that book. It's in between Nagel & Newman's popular exposition and the dense presentation you find in math logic texts like Mendelson's. I recall that he specifically discusses Presburger arithmetic and the issues you raise here.

Answer by Kristal Cantwell for Presburger Arithmetic

2009-12-27T21:21:00Z

Presburger introduced his arithmetic in 1929 the paper was translated into English in 1991. Here is the citation to this paper:

M. Presburger. Ueber die Vollstaendigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. C.R. du I Congr. des Math. des pays Slaves, Warszawa, 1929, pp.92-101

Here is the english translation:

On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation Mojżesz Presburger; Dale Jabcquette History and Philosophy of Logic, 1464-5149, Volume 12, Issue 2, 1991, Pages 225 – 233

The pdf here which is mentioned in Jason Dyer's comment to the original question states that in the paper above the system is used to prove its own consistency.

He reduced all statements in his arithmetic to quantifier free statements. To do this he add to extend the system by introducing modular equivalence. The result was a reduction of every statement to the quantifier free form. This led to an algorithm for deciding every statement. There is in fact bounds on the efficiency of the decision algorithm algorithm. It is greater than double exponential and less than triple exponential. For the lower bound see:

M. J. Fischer, M. O. Rabin. Super-Exponential Complexity of Presburger Arithmetic. "Proceedings of the SIAM-AMS Symposium in Applied Mathematics", 1974, vol. 7, pp.27-41

For the upper bound see:

Derek C. Oppen: A 2^2^2^pn Upper Bound on the Complexity of Presburger Arithmetic. J. Comput. Syst. Sci. 16(3): 323-332 (1978)

For there to be inconsistency there would have to be a finite set of inconsistent modular statements. Because of this it is plausible to me that the original paper used the extended system to prove its own consistency.

Answer by Neel Krishnaswami for Presburger Arithmetic

2009-12-29T12:25:57Z

Presburger arithmetic does NOT prove its own consistency. Its only function symbols are addition and successor, which are not sufficient to represent Godel encodings of propositions.

However, consistent self-verifying axiom systems do exist -- see the work of Dan Willard ("Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles"). The basic idea is to include enough arithmetic to make Godel codings work, but not enough to make the incompleteness theorem go through. In particular, you remove the addition and multiplication function symbols, and replace them with subtraction and division. This is enough to permit representing the theory arithmetically, but the totality of multiplication (which is essential for the proof of the incompleteness theorem) is not provable, which lets you consistently add a reflection principle to the logic.

Answer by Doukas for Presburger Arithmetic

2010-06-22T20:27:05Z

I like the discussion. (I am currently working on similar themes.) I have come to the following conclusions. In order for a theory to be provably consistent, it needs either (i) to be provably consistent but not by itself, like in Presburger or in Peano, or (ii) to be provably consistent by itself but in that case the theory has to disallow the inference from the statement that it is consistent to the I am improvable sentence, like in Willard. The introduction of the reflection principle is possible there exactly because of what you say Adam. Notice that in case the fixed point theorem did work in Willard, this, in combination with the reflection principle, would suffice for a contradiction, and no matter what the status of the first incompleteness theorem would be.