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

Tue Apr 12 07:34:14 EDT 2011

On 2011年4月11日 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:
http://mathworld.wolfram.com/PeanoArithmetic.html
Oh, and this may be of interest:
http://scienceblogs.com/goodmath/2006/06/extreme_math_1_1_2.php
-- 
Steven