You might contact Jeanne Ferrante, who wrote the following with Charles Rackoff: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics 718 Pressburger Arithmetic is pretty well behaved, and some fragments are now used for proving theorems about index arithmetic in 'for' loops in compilers. http://en.wikipedia.org/wiki/Presburger_arithmetic You might also look at "S1S" and "S2S" as possible inspirations: From: http://www.cs.tau.ac.il/~rabinoa/seminar11/s2s.pdf Size: 1.2 MB (1,239,226 bytes) At 11:05 AM 9/3/2013, James Propp wrote:

Are there (positive) integers m,n definable in PA whose existence is provable in PA such that m \geq n and n \geq m are undecidable in PA? (I think that's the right way to ask the question I have in mind, but if my wording evinces misunderstanding of foundational issues, please enlighten me!)

What if we replace PA by a stronger theory?

The underlying intuition is that if there are incomprehensibly big numbers, at some point even comparative notions of bigness should start to fail us, so that, in a certain sense, the well-ordering of the natural numbers should become problematical.

But my intuitions may be totally off-base...

Jim Propp