[even more OT than before] Arithmetic [was Free software versus software idea patents]

Steven D'Aprano steve+comp.lang.python at pearwood.info
Tue Apr 12 07:34:14 EDT 2011

On Mon, 11 Apr 2011 15:55:37 -0700, geremy condra wrote:

>> Ah, I didn't know that! How wonderful! But in any case, Presburger
>> arithmetic is much weaker than even Peano arithmetic.
>> http://en.wikipedia.org/wiki/Presburger_arithmetic
>> So, let me re-phrase my statement... in any realistically complex
>> arithmetic that is consistent with operations performed for real-world
>> applications (e.g. multiplication, division, exponentiation, ...), one
>> cannot demonstrate a bullet-proof proof of 1+1=2. Better? :)
> Well, Peano arithmetic is normal, everyday arithmetic fully axiomatized,
> and Presburger arithmetic is a subset of it, so we can utilize the fact
> that 1 + 1 = 2 is provable in Presburger arithmetic (damn is my spell
> checker getting a workout on this sentence) to prove it in Peano
> arithmetic, and therefore in everyday use.

Alas, that's not the case. Peano arithmetic is undecidable:


Oh, and this may be of interest:


More information about the Python-list mailing list