The countable reals

53 views
Skip to first unread message

andrej...@andrej.com

unread,
Apr 2, 2024, 4:11:59 AMApr 2
to Constructive news
Dear friends,

James Hanson and I have finally publish a preprint “The Countable Reals”:

https://arxiv.org/abs/2404.01256

We construct a topos in which the Dedekind reals are countable.

The topos invalidates excluded middle and countable choice (as it must). It is quite strange:

* the Hilbert cube [0,1]^ω is countable
* from which we get Brouwer’s fixed point theorem as a consequence of Lawvere’s fixed-point theorem
* therefore the intermediate value theorem and analytic LLPO hold
* [0,1] has a singular cover (that is trival to construct), but
* every countable cover of [0,1] by open intervals with *rational* endpoints has a finite subcover.

We also claim KLST theorem “all maps are continuous”, but there’s a problem with the latter part of the proof, which we hope to fix soon and upload a new version.

There are many other things that we do not know about the topos.

With kind regards,

Andrej

Henri Lombardi

unread,
May 27, 2024, 11:06:42 AMMay 27
to Constructive news


C'est avec émotion que j'ai appris le décès de Fred Richman. Il a été pour moi ce que l'on appelle un « ami mathématique ».

Il m'avait envoyé quelques premières versions de chapitres de son livre avec Mines et Ruitenburg alors même que je préparais ma thèse (soutenue à 44 ans, après ma découverte du livre de Bishop qui m'avait réconcilié avec les mathématiques). J'avais tout de suite été conquis par son style si clair et élégant. J'y ai découvert le fait que la caractéristique d'un corps bien construit pouvait n'être pas bien définie. Il s'était déclaré amusé par ma construction d'un anneau qui hésitait entre le corps fini F_3 et le corps des entiers 3-adiques Q_3

Depuis, nous avons entretenu une correspondance régulière. Sa disponibilité, sa gentillesse et son efficacité m'ont toujours impressionné.

J'ai eu le plaisir de rédiger un commentaire du livre A Course in Constructive Algebra pour le Handbook of Constructive Mathematics récemment paru (voir arXiv:1903.04200). J'ai aussi eu l'honneur de traduire en français cet ouvrage merveilleux (CCA), avec l'aide de mon collègue Stefan Neuwirth. Fred a toujours répondu de manière très précise aux demandes d'éclaircissement que nous avons formulées.

C'était aussi un spécialiste des contrexemples brouwériens souvent si utiles à la compréhension de points délicats, qui répondait toujours très rapidement aux questions que je lui posais.

Je citerai parmi ses articles qui m'ont fortement marqué :
• Constructive aspects of Noetherian rings. Proc. Amer. Mat. Soc. 44 (1974), 436–441.
• Church Thesis without tears. Journal of Symbolic Logic 48 (3) (1983), 797–803.
• Meaning and information in constructive mathematics. Am. Math. Mon., 89 :385–388, (1982).
• Non trivial uses of trivial rings. Proc. Amer. Math. Soc. 103 (1988), 1012–1014.
• Intuitionism as generalization. Philosophia Mathematica 5 (1990), 124–128.
• Fred Richman and Douglas Bridges. A constructive proof of Gleason’s theorem. J. Funct. Anal., 162(2) :287–312, (1999).
• The fundamental theorem of algebra : a constructive development without choice. Pac. J. Math., 196(1) :213–230, (2000).
• Constructive mathematics without choice. In Reuniting the antipodes—constructive and nonstandard views of the continuum. Symposium proceedings, San Servolo, Venice, Italy, May 16–22, 1999, pages 199–205. Dordrecht : Kluwer Academic Publishers, (2001)
• The ascending tree condition : constructive algebra without countable choice. Commun. Algebra, 31(4) :1993–2002, (2003).
• David Pengelley and Fred Richman. Did Euclid need the Euclidean algorithm to prove unique factorization ? Amer. Math. Monthly, 113(3) :196– 205, 2006.

Enfin, il me fit l'honneur de faire le voyage en Europe, en 2011 à Besançon, pour participer à la petite fête donnée pour ma retraite et mes 65 ans. Il fit un bel exposé sur la manière de construire des anneaux d' interpolation qui hésitent entre différentes structures selon qu'une suite binaire infinie est identiquement nulle ou pas.
Voir http://epiphymaths.univ-fcomte.fr/fete-a-henri/Richman-Besancon.pdf


Henri


Fred.pdf

Henri Lombardi

unread,
Jun 26, 2024, 10:38:39 AMJun 26
to Constructive news, Henri Lombardi, Assia Mahboubi, Claude Quitté, Maria Emilia Alonso Garcia, Gema Diaz, Lalo Gonzalez-Vega, Marie-Francoise Roy, Michel Coste, Stefan Neuwirth, Thierry Coquand, Tomas Recio, Reichenberger, Andrea, Dr.
Dear all

We have a paper in french, Assia and myself, about
"what is a good geometric for the real number field"

the real number field has no sign test

moreover we agree with the critics by Fred and we think that it is better to drop dependant choice

the usual formal first order theory of real closed fields is based on the zero test
which is not available for Cauchy-Bishop real numbers

Henri


Your submission submit/5683693 has been assigned the permanent arXiv
identifier 2406.15218 and is available at:

http://arxiv.org/abs/2406.15218
Reply all
Reply to author
Forward
0 new messages