Presburger Arithmetic 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.
 A: 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.
A: 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. 
A: 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.  
