lo.logic - Presburger Arithmetic

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.