Path: csiph.com!x330-a1.tempe.blueboxinc.net!usenet.pasdenom.info!aioe.org!feeder.news-service.com!newsfeed.xs4all.nl!newsfeed5.news.xs4all.nl!xs4all!post.news.xs4all.nl!not-for-mail
DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=nneWV8SXF9N8lGwRvBFKekxGPXdCKCfMTl4UoBhrmhoBcbNa7tqlXo2A5tQp9md+ia 8UubOpKCzKw/DZu/gyEx5kyKToMJlKfLvaYpr9VGi8z6OkSzWKnQEDtmLVtZRhTzTjKw wJuekfDFIAmWl4kVjfJZfgcHQ50DMllWxLGzU=
MIME-Version: 1.0
In-Reply-To: <4da380a4$0$29982$c3e8da3$5496439d@news.astraweb.com>
References: <mailman.65.1302065189.9059.python-list@python.org> <t7Vmp.7632$zn.3197@newsfe19.iad> <mailman.72.1302078388.9059.python-list@python.org> <4d9c5ca5$0$29991$c3e8da3$5496439d@news.astraweb.com> <87tyebf3r3.fsf_-_@benfinney.id.au> <_Abnp.8356$zn.729@newsfe19.iad> <4d9d6587$0$29992$c3e8da3$5496439d@news.astraweb.com> <OHlnp.10535$g56.5872@newsfe04.iad> <mailman.121.1302206148.9059.python-list@python.org> <__top.14604$zn.8052@newsfe19.iad> <mailman.209.1302508440.9059.python-list@python.org> <4da2c58a$0$29965$c3e8da3$5496439d@news.astraweb.com> <mailman.223.1302545833.9059.python-list@python.org> <4da380a4$0$29982$c3e8da3$5496439d@news.astraweb.com>
Date: Mon, 11 Apr 2011 15:55:37 -0700
Subject: Re: [OT] Free software versus software idea patents
From: geremy condra <debatem1@gmail.com>
To: "Steven D'Aprano" <steve+comp.lang.python@pearwood.info>
Content-Type: text/plain; charset=ISO-8859-1
Cc: python-list@python.org
Precedence: list
Newsgroups: comp.lang.python
Message-ID: <mailman.229.1302562540.9059.python-list@python.org>
Lines: 53
NNTP-Posting-Host: 82.94.164.166
Xref: x330-a1.tempe.blueboxinc.net comp.lang.python:3001

On Mon, Apr 11, 2011 at 3:28 PM, Steven D'Aprano
<steve+comp.lang.python@pearwood.info> wrote:
> On Mon, 11 Apr 2011 11:17:09 -0700, geremy condra wrote:
>
>> On Mon, Apr 11, 2011 at 2:10 AM, Steven D'Aprano
>> <steve+comp.lang.python@pearwood.info> wrote:
> [...]
>>> Of course, some mathematics is obvious, or at least intuitive (although
>>> proving it rigorously can be remarkably difficult -- after 4000 years
>>> of maths, we still don't have an absolutely bullet-proof proof that
>>> 1+1=2).
>>
>> Erm. This is getting a bit far afield, but yes, we do. The statement you
>> provide above part of Presbuger arithmetic, which is both complete and
>> decidable.
>
> 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.

You'd also be surprised what you can do with some limited arithmetic
forms. During my undergrad I spent some time writing a Presburger
prover that was actually fairly handy- there are definitely instances
where trading multiplication by non-constant factors for provability
superpowers is a good deal.

> Presburger arithmetic, Peano arithmetic, the Axiom of Choice... we're
> getting further and further away from "natural" mathematics, e.g.
> counting sheep in a field.

Yes, the sheep would much rather hear about patent reform than the
axiom of choice ;)

<snip>

> Anyway, this is now getting off-topic even for the original off-topic
> post. Time to move on, methinks.

Yeah, looks like a good time to let this one trail off.

Geremy Condra