26
$\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.

Improve this question
$\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$
    – Theo Johnson-Freyd
    Commented 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$
    – David E Speyer
    Commented 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
    Commented 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$
    – Brendan Cordy
    Commented 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$
    – Brendan Cordy
    Commented Dec 27, 2009 at 16:39

3 Answers 3

Reset to default
41
$\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

  • Dan E. Willard, Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles, The Journal of Symbolic Logic. 66 (2) (2001) pp 536–596. doi:10.2307/2695030, JSTOR, (author pdf).

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.

Improve this answer
$\endgroup$
7
  • $\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$
    – Brendan Cordy
    Commented Dec 29, 2009 at 16:43
  • 8
    $\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
    Commented 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
    Commented Aug 26, 2023 at 20:50
  • 7
    $\begingroup$ @plm The wording that Presburger arithmetic “does not prove its own consistency” is misleading. The issue is not whether Presburger arithmetic can or cannot prove something, but that there is no statement to be proved in the first place, as the language of Presburger arithmetic is not expressive enough that it could even formulate its own consistency in a meaningful way. This is not a formal theorem, so there is no way a reference could “prove” it, as it depends on subjective criteria on what counts as an honest formalization of a consistency statement in a language of arithmetic. $\endgroup$
    – Emil Jeřábek
    Commented Apr 17 at 12:31
  • 2
    $\begingroup$ Of course, you can decide that, for example, the sentence “0=0” is a formalization of the consistency of Presburger arithmetic, and then Presburger arithmetic can prove it. But you will not find many people to agree that this is a faithful formalization of the notion of consistency. $\endgroup$
    – Emil Jeřábek
    Commented Apr 17 at 12:33
8
$\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 book An Introduction to Gödel's Theorems for starters to get clear on this stuff.

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.

Improve this answer
$\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$
    – Brendan Cordy
    Commented 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$
    – Brendan Cordy
    Commented 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:

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

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 https://doi.org/10.1007/978-3-7091-9459-1_5

For the upper bound see:

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.

Improve this answer
$\endgroup$
3
  • 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$
    – Brendan Cordy
    Commented 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$
    – Brendan Cordy
    Commented Dec 28, 2009 at 5:16
  • $\begingroup$ Do you know by any chance if there are explicit estimates for the constant in the Fischer-Rabin bound? $\endgroup$
    – Mikhail Katz
    Commented Nov 6 at 11:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .