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.



Presburger Arithmetic
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"](http://www.cs.albany.edu/~dew/m/jsl1.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. 


