Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.python > #95175
| 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 | 2015-08-09 00:27 +0300 |
| Organization | A noiseless patient Spider |
| Message-ID | <87614po4ij.fsf@elektro.pacujo.net> (permalink) |
| References | (6 earlier) <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> |
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
Back to comp.lang.python | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
Re: Should non-security 2.7 bugs be fixed? Devin Jeanpierre <jeanpierreda@gmail.com> - 2015-07-18 19:33 -0700
Re: Should non-security 2.7 bugs be fixed? Rick Johnson <rantingrickjohnson@gmail.com> - 2015-07-18 19:49 -0700
Re: Should non-security 2.7 bugs be fixed? Rustom Mody <rustompmody@gmail.com> - 2015-07-18 20:52 -0700
Re: Should non-security 2.7 bugs be fixed? Rick Johnson <rantingrickjohnson@gmail.com> - 2015-07-18 21:18 -0700
Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Steven D'Aprano <steve@pearwood.info> - 2015-07-19 14:45 +1000
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Chris Angelico <rosuav@gmail.com> - 2015-07-19 15:06 +1000
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-07-19 10:16 +0300
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-19 00:32 -0700
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-07-19 10:44 +0300
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Terry Reedy <tjreedy@udel.edu> - 2015-07-19 19:13 -0400
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-19 19:02 -0700
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Anuradha Laxminarayan <lanuradha@gmail.com> - 2015-07-18 23:25 -0700
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Terry Reedy <tjreedy@udel.edu> - 2015-07-19 04:26 -0400
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Tim Chase <python.list@tim.thechases.com> - 2015-07-19 07:56 -0500
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Chris Angelico <rosuav@gmail.com> - 2015-07-20 04:07 +1000
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Tim Chase <python.list@tim.thechases.com> - 2015-07-19 14:55 -0500
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Chris Angelico <rosuav@gmail.com> - 2015-07-20 07:16 +1000
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] wxjmfauth@gmail.com - 2015-07-20 00:43 -0700
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] MRAB <python@mrabarnett.plus.com> - 2015-07-19 23:13 +0100
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-20 20:30 -0700
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Chris Angelico <rosuav@gmail.com> - 2015-07-21 13:43 +1000
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-20 23:11 -0700
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Laura Creighton <lac@openend.se> - 2015-07-21 10:10 +0200
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-07-21 12:10 +0300
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Chris Angelico <rosuav@gmail.com> - 2015-07-21 19:18 +1000
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-07-21 13:13 +0300
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-07-21 11:34 +0100
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2015-07-21 20:39 +1000
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-07-21 13:54 +0300
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-08-09 00:27 +0300
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-08-09 09:29 -0700
Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-22 06:34 -0700
OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Steven D'Aprano <steve@pearwood.info> - 2015-07-23 02:58 +1000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Laura Creighton <lac@openend.se> - 2015-07-22 19:17 +0200
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-22 10:49 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Laura Creighton <lac@openend.se> - 2015-07-22 20:14 +0200
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-07-22 21:59 +0100
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Steven D'Aprano <steve@pearwood.info> - 2015-07-23 03:21 +1000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Dennis Lee Bieber <wlfraed@ix.netcom.com> - 2015-07-22 21:44 -0400
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Chris Angelico <rosuav@gmail.com> - 2015-07-23 12:00 +1000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Paul Rubin <no.email@nospam.invalid> - 2015-07-22 10:48 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-22 10:51 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2015-07-23 15:14 +1000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-22 11:09 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2015-07-23 15:41 +1000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-07-23 23:59 +0300
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Chris Angelico <rosuav@gmail.com> - 2015-07-24 07:03 +1000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-07-24 00:29 +0300
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-07-23 22:50 +0100
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Laura Creighton <lac@openend.se> - 2015-07-23 23:52 +0200
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-07-24 00:59 +0300
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Chris Angelico <rosuav@gmail.com> - 2015-07-24 08:02 +1000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Chris Angelico <rosuav@gmail.com> - 2015-07-24 08:00 +1000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] MRAB <python@mrabarnett.plus.com> - 2015-07-23 23:01 +0100
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Laura Creighton <lac@openend.se> - 2015-07-24 00:19 +0200
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-07-23 23:56 +0100
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Grant Edwards <invalid@invalid.invalid> - 2015-07-24 00:07 +0000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rick Johnson <rantingrickjohnson@gmail.com> - 2015-07-23 18:40 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Paul Rubin <no.email@nospam.invalid> - 2015-07-23 19:03 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rick Johnson <rantingrickjohnson@gmail.com> - 2015-07-23 20:16 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Grant Edwards <invalid@invalid.invalid> - 2015-07-24 14:13 +0000
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Paul Rubin <no.email@nospam.invalid> - 2015-07-24 08:45 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-07-24 16:58 +0100
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-23 22:15 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Gregory Ewing <greg.ewing@canterbury.ac.nz> - 2015-07-23 18:57 +1200
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-23 02:12 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Rustom Mody <rustompmody@gmail.com> - 2015-07-23 05:52 -0700
Re: OT Re: Math-embarrassment results in CS [was: Should non-security 2.7 bugs be fixed?] Marko Rauhamaa <marko@pacujo.net> - 2015-07-23 11:24 +0300
Re: Devanagari int literals [was Re: Should non-security 2.7 bugs be fixed?] Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2015-07-21 18:57 +1000
Re: Should non-security 2.7 bugs be fixed? Terry Reedy <tjreedy@udel.edu> - 2015-07-19 02:44 -0400
Re: Should non-security 2.7 bugs be fixed? Terry Reedy <tjreedy@udel.edu> - 2015-07-19 05:11 -0400
Re: Should non-security 2.7 bugs be fixed? Rustom Mody <rustompmody@gmail.com> - 2015-07-19 07:30 -0700
Re: Should non-security 2.7 bugs be fixed? Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-07-19 15:00 +0100
Re: Should non-security 2.7 bugs be fixed? Steven D'Aprano <steve@pearwood.info> - 2015-07-19 14:45 +1000
Re: Should non-security 2.7 bugs be fixed? Devin Jeanpierre <jeanpierreda@gmail.com> - 2015-07-19 18:20 -0700
Re: Should non-security 2.7 bugs be fixed? Steven D'Aprano <steve@pearwood.info> - 2015-07-20 13:05 +1000
Re: Should non-security 2.7 bugs be fixed? Devin Jeanpierre <jeanpierreda@gmail.com> - 2015-07-19 20:41 -0700
Re: Should non-security 2.7 bugs be fixed? Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-07-20 02:46 +0100
Re: Should non-security 2.7 bugs be fixed? Rustom Mody <rustompmody@gmail.com> - 2015-07-19 19:16 -0700
Re: Should non-security 2.7 bugs be fixed? Chris Angelico <rosuav@gmail.com> - 2015-07-20 12:59 +1000
Re: Should non-security 2.7 bugs be fixed? Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-07-20 11:59 +0100
Re: Should non-security 2.7 bugs be fixed? Rick Johnson <rantingrickjohnson@gmail.com> - 2015-07-20 20:04 -0700
Re: Should non-security 2.7 bugs be fixed? Rustom Mody <rustompmody@gmail.com> - 2015-07-20 20:15 -0700
Re: Should non-security 2.7 bugs be fixed? Chris Angelico <rosuav@gmail.com> - 2015-07-21 13:33 +1000
Re: Should non-security 2.7 bugs be fixed? Terry Reedy <tjreedy@udel.edu> - 2015-07-21 00:45 -0400
Re: Should non-security 2.7 bugs be fixed? breamoreboy@gmail.com - 2015-07-21 14:22 -0700
Re: Should non-security 2.7 bugs be fixed? Rick Johnson <rantingrickjohnson@gmail.com> - 2015-07-21 19:07 -0700
Re: Should non-security 2.7 bugs be fixed? Terry Reedy <tjreedy@udel.edu> - 2015-07-22 02:51 -0400
Re: Should non-security 2.7 bugs be fixed? Rick Johnson <rantingrickjohnson@gmail.com> - 2015-07-22 16:37 -0700
Re: Should non-security 2.7 bugs be fixed? Terry Reedy <tjreedy@udel.edu> - 2015-07-20 02:25 -0400
Re: Should non-security 2.7 bugs be fixed? dieter <dieter@handshake.de> - 2015-07-20 08:58 +0200
Re: Should non-security 2.7 bugs be fixed? Devin Jeanpierre <jeanpierreda@gmail.com> - 2015-07-20 00:13 -0700
csiph-web