Path: csiph.com!eternal-september.org!feeder.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Marko Rauhamaa <marko@pacujo.net>
Newsgroups: comp.lang.python
Subject: Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?]
Date: Sun, 09 Aug 2015 00:27:00 +0300
Organization: A noiseless patient Spider
Lines: 54
Message-ID: <87614po4ij.fsf@elektro.pacujo.net>
References: <moenuj$f11$1@ger.gmane.org> <moeqtn$mh0$1@ger.gmane.org> <moeurf$a6f$1@ger.gmane.org> <mailman.695.1437273248.3674.python-list@python.org> <7083e494-6192-4acb-aea9-216d858171bc@googlegroups.com> <55ab2b57$0$1664$c3e8da3$5496439d@news.astraweb.com> <76252f32-64e9-405b-84a2-996200a6fa6f@googlegroups.com> <mailman.808.1437466239.3674.python-list@python.org> <87twsxj2ot.fsf@elektro.pacujo.net> <55ae2171$0$1646$c3e8da3$5496439d@news.astraweb.com> <87h9oxixwy.fsf@elektro.pacujo.net>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: mx02.eternal-september.org; posting-host="b7cb1518d23ec19d482dcc9c31d30fdd"; logging-data="19446"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18zQKc/GqjCdSifZyduzrp5"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:npv02qSCl3CuksJaccJyl/AMBqM= sha1:zd3jaj4fTHbeLotKMlQABsr2HKE=
Xref: csiph.com comp.lang.python:95175

Marko Rauhamaa <marko@pacujo.net>:

> Steven D'Aprano <steve+comp.lang.python@pearwood.info>:
>
>> The contemporary standard approach is from Zermelo-Fraenkel set
>> theory: define 0 as the empty set, and the successor to n as the
>> union of n and the set containing n:
>>
>> 0 = {} (the empty set) 
>> n + 1 = n ∪ {n}
>
> That definition barely captures the essence of what a number *is*. In
> fact, there have been different formulations of natural numbers.

Rehashing this old discussion. I ran into this wonderful website:

  <URL: http://at.metamath.org/mpeuni/mmset.html>

It is an absolute treasure for those of us who hate handwaving in math
textbooks. The database of computer-checked theorems proves everything
starting from the very bottom.

An interesting, recurring dividing line among the proofs is a layer of
"provable" axioms. For example, this proof

   http://at.metamath.org/mpeuni/2p2e4.html

(for "⊢ (2 + 2) = 4") references the axiom (<URL:
http://at.metamath.org/mpeuni/ax-1cn.html>):

   ⊢ 1 ∈ ℂ

The axiom is "justified by" a set-theoretic theorem:

   Description: 1 is a complex number. Axiom 2 of 22 for real and
   complex numbers, derived from ZF set theory. This
   construction-dependent theorem should not be referenced directly;
   instead, use ax-1cn 7963.
   <URL: http://at.metamath.org/mpeuni/ax1cn.html>

In other words, since there is no canonical way to define numbers in set
theory, Metamath insulates its proofs from a particular definition by
circumscribing numbers with construction-independent axioms.


Anyway, ob. Python reference:

   Using the design ideas implemented in Metamath, Raph Levien has
   implemented what might be the smallest proof checker in the world,
   mmverify.py, at only 500 lines of Python code.
   <URL: https://en.wikipedia.org/wiki/Metamath>


Marko