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

[Steven D'Aprano]

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:

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