25
$\begingroup$

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.

$\endgroup$
7
  • 1
    $\begingroup$ All I know is what I've read in the Wikipedia page (en.wikipedia.org/wiki/Presburger_arithmetic), which is the first hit on Google for "presburger arithmetic". It lists many references, and attributes the claims in your question to the original paper by Presburger (in German). $\endgroup$ Dec 27, 2009 at 9:16
  • 5
    $\begingroup$ I may be being dumb here but: I don't see this statement in the wikipedia summary. Wikipedia says that Presburger showed that Presburger arithmetic is consistent, but it doesn't say that this fact can be proved, or even expressed, in Presburger arithmetic. $\endgroup$ Dec 27, 2009 at 13:01
  • $\begingroup$ I did find one source for "proves its own consistency", but I don't know how reliable it is. staff.science.uva.nl/~suckelma/teaching/CL2008/2008-CL-L12.pdf $\endgroup$
    – Jason Dyer
    Dec 27, 2009 at 16:20
  • $\begingroup$ Remember that we can prove the consistency of Peano arithmetic as well, but not within Peano arithmetic. Gentzen did it by ordinal induction on $\epsilon_0$. $\endgroup$ Dec 27, 2009 at 16:38
  • $\begingroup$ I could be wrong about that claim, perhaps there is no way to express the consistency of Presburger arithmetic with a sentence of Presburger arithmetic. If so, I'd like to know precisely why. $\endgroup$ Dec 27, 2009 at 16:39

3 Answers 3

37
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Thanks. I think that reference is exactly the kind of thing I'm looking for. I know a few ways to make Godel codings work for PA, but I've never seen any results about precisely when such an encoding is not possible. $\endgroup$ Dec 29, 2009 at 16:43
  • 7
    $\begingroup$ I spent a good while reading Willard's papers trying to figure out exactly why it worked. I came to the conclusion that the "trick" is that omitting totality of multiplication breaks what has come to be called "Godel's Fixed Point Theorem" (see "Theorem 2" at plato.stanford.edu/entries/goedel for a nice statement) but breaks as little else of Peano Arithmetic as possible. Can anybody confirm whether or not this is the essential feature of his work? If it is, I really wish he had said so in his abstracts! :) $\endgroup$
    – Adam
    Jan 1, 2010 at 20:47
  • $\begingroup$ Dear Neel, Do you have a reference that proves that Presburger arithmetic does not (ie cannot) prove its own consistency ? That seems plausible (as PrA does not represent all primitive recursive functions, and not even multiplication nor division) but not trivial to me. The fact that the habitual (type of) method used in PA (Gödel encoding and manipulations with Gödel numbers) cannot be used in PrA does not (obviously) tell us that some other encoding cannot exist. $\endgroup$
    – plm
    Aug 26, 2023 at 20:50
7
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thanks for the reference; I'll grab it from a library. My favourite introductory logic text is Van Dalen's, which ends with an in depth development of the first incompleteness theorem for PA, but doesn't talk about other theories of arithmetic. $\endgroup$ Dec 27, 2009 at 20:09
  • $\begingroup$ If there is a proof of the consistency of Presburger arithmetic in some metalanguage which assumes only the well-foundedness of $\omega$, then one could say that Presburger arithmetic 'proves it's own consistency', since it proves that $\omega$ is well founded (This is equivalent to being able to perform induction on $\omega$, which is actually an axiom of Presburger arithmetic). $\endgroup$ Dec 27, 2009 at 20:09
5
$\begingroup$

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.

$\endgroup$
2
  • 2
    $\begingroup$ I know that Presburger arithmetic has quantifier elimination and is decidable. This is quite nice, as it gives a quick way of showing consistency, namely, just check that the sentence $0 \neq 1$ is not a theorem. However, this proof of consistency uses the notion of decidability, so we have to step outside the realm of what can be done with Presburger arithmetic. $\endgroup$ Dec 28, 2009 at 5:12
  • $\begingroup$ With regards to the last paragraph: Still it seems to me that the problem comes down to the fact that there's no obvious way, using only the language of Presburger arithmetic, to say that finite set of statements in Presburger arithmetic with modular equivalence is inconsistent. $\endgroup$ Dec 28, 2009 at 5:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.