Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?]
Marko Rauhamaa
marko at pacujo.net
Sat Aug 8 17:27:00 EDT 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;
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
More information about the Python-list
mailing list