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

Marko Rauhamaa marko at pacujo.net
Sat Aug 8 23:27:00 CEST 2015

```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;
<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
```