Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?]

[Marko Rauhamaa]

Marko Rauhamaa <marko at pacujo.net>:

> Steven D'Aprano <steve+comp.lang.python at 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