On Tue, Apr 12, 2011 at 4:34 AM, Steven D'Aprano <steve+comp.lang.pyt...@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 -- http://mail.python.org/mailman/listinfo/python-list