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

[geremy condra]

On Tue, Apr 12, 2011 at 4:34 AM, Steven D'Aprano
<steve+comp.lang.python at pearwood.info> wrote:
> 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

Presburger arithmetic is a subset of Peano Arithmetic, ie, all
statements which are true in Presburger Arithmetic are true in Peano
arithmetic, and all statements which are false in Presburger
arithmetic are false in Peano arithmetic. A bullet-proof proof of the
fact you listed exists in Presburger arithmetic. By implication the
statement is therefore proven true in Peano arithmetic.

Also, undecidable does not mean that *no* statement can be proven
formally true or false, only that statements which cannot be proven
true or false exist within the confines of those axioms, ie, an
axiomatic system is undecidable if there exists an expressible
statement within it that is independent of all of the axioms. As you
note below, there are other proofs under ZF (and optionally C).

> Oh, and this may be of interest:
> http://scienceblogs.com/goodmath/2006/06/extreme_math_1_1_2.php

It's fine until you get to the end, then it drops into a completely
incorrect interpretation both of what R&W were doing and of Godel's
work.

By the way, if you're interested in this sort of thing, Paul Bernays'
(the 'B' in NBG set theory, the other two being no less than von
Neumann and Godel) book on axiomatic set theory is cheaply available
through Dover and is really, really good at getting to the meat on
this sort of thing.

Geremy Condra