[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:
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
More information about the Python-list
mailing list