Email Gateway (Nov 01 2023 at 16:46): Email Gateway (Nov 01 2023 at 16:46):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce a new AFP entry, by Ata Keskin:
Eudoxus Reals
Similar to the classical method of Dedekind cuts, our approach starts from first principles. However, unlike Dedekind cuts, Eudoxus reals directly derive real numbers from integers, bypassing the intermediate step of constructing rational numbers. This construction of the real numbers was first discovered by Stephen Schanuel. Schanuel named his construction after the ancient Greek philosopher Eudoxus, who developed a theory of magnitude and proportion to explain the relations between the discrete and the continuous. Our formalization is based on R.D. Arthan's paper detailing the construction. For establishing the existence of multiplicative inverses for positive slopes, we used the idea of finding a suitable representative from Sławomir Kołodyńaski's construction on IsarMathLib which is based on Zermelo-Fraenkel set theory. Up to this date, our formalization is the only construction of Eudoxus reals which is based on HOL.
Curiously enough, I've wanted to see this sort of construction for several decades. NG de Bruijn once mentioned to me his own construction of the real numbers without the rationals:
N.G de Bruijn,
Defining reals without the use of rationals,
Indagationes Mathematicae Volume 79, Issue 2, 1976,
https://doi.org/10.1016/1385-7258(76)90055-X.
Interesting references in that paper, too. So thanks to Ata!
Anyway, the entry is online at https://www.isa-afp.org/entries/Eudoxus_Reals.html
Larry Paulson
Email Gateway (Nov 04 2023 at 02:43):From: Ken Kubota <mail@kenkubota.de>
I have to say that I find it inappropriate to continue with routine work currently.
The New York U.N. representative wrote concerning Gaza: "This is a text-book case of genocide.“
https://www.documentcloud.org/documents/24103463-craig-mokhiber-resignation-letter
This is confirmed by brilliant analysts such as the former CIA analyst Ray McGovern:
https://odysee.com/@SputnikInternational:c/New-Rules-Ray-McGovern:f?t=100
Doesn’t the University of Cambridge officially condemn this act of genocide?
While generally science should be autonomous to a certain degree, there are limits.
Particularly in times where public protests effectively can make a difference.
Bertrand Russell wasn’t indifferent:
https://sonar21.com/lord-bertrand-russells-on-israels-miscalculation/
Some more information is provided below.
Ken Kubota
https://doi.org/10.4444/100
Links:
https://marlene.hilsenrath.de/blog/gaza-genocide/
https://www.mintpressnews.com/craig-murray-israel-genocide-gaza-regional-war-unavoidable/286129/
https://odysee.com/@SputnikInternational:c/New-Rules-Ray-McGovern:f?t=100
https://www.ohchr.org/en/press-releases/2023/10/gaza-un-experts-decry-bombing-hospitals-and-schools-crimes-against-humanity
https://rumble.com/v3r6kw7-judge-napolitano-judging-freedom-ray-mcgovern-blinken-goes-berserk.html?start=468
https://rumble.com/v3poopd-judge-napolitano-judging-freedom-us-aid-is-destroying-ukraine.-w-ray-mcgove.html?start=588
https://odysee.com/@LandDestroyer:8/the-2009-us-plan-for-iran-war-sees-new:d
https://www.youtube.com/live/iq1SjC7u8l0?t=126
https://www.sevimdagdelen.de/toedliche-doppelmoral/
https://www.documentcloud.org/documents/24103463-craig-mokhiber-resignation-letter
From: https://www.tiktok.com/@marlenehilsenrath/video/7297390486308818208
Last updated: Apr 29 2024 at 01:08 UTC