The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

This might be relevant to some other mailing lists as well.

Anfang der weitergeleiteten Nachricht:

Von: Ken Kubota <mail AT kenkubota.de>

Betreff: Aw: [isabelle] New in the AFP: Eudoxus Reals

Datum: 4. November 2023 um 03:34:06 MEZ

An: "Prof. Lawrence C. Paulson" <lp15 AT cam.ac.uk>

Kopie: isabelle-users <cl-isabelle-users AT lists.cam.ac.uk>

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

Am 01.11.2023 um 17:45 schrieb Lawrence Paulson <lp15 AT 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