Synthetic Mathematics I

Andrej Bauer is our delightful guest in this long episode! We talk about intuitionistic logic, and how adopting an open minded attitude towards foundations of logic can help you discover new mathematical worlds! Andrej has an incredible aptitude for taking complex ideas in logic and making them simple and compelling. Here are some links to know more: https://www.andrej.com/ https://math.andrej.com/ This is Part I of our episode. A few of the works referenced in our chat: 1. The Countable Reals https://arxiv.org/abs/2404.01256 Andrej Bauer, James E. Hanson 2. On Fixed-Point Theorems in Synthetic Computability https://math.andrej.com/asset/data/recursion-theorem.pdf Andrej Bauer 3. An Invitation to Smooth Infinitesimal Analysis https://publish.uwo.ca/\~jbell/invitation%20to%20SIA.pdf John L. Bell 4. Constructive Analysis https://link.springer.com/book/10.1007/978-3-642-61667-9 Errett Bishop, Douglas Bridges 5. An introduction to fibrations, topos theory, the effective topos and modest sets https://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ Wesley Phoa 6. The Effective Topos https://www.dpmms.cam.ac.uk/~jmeh1/Research/Pub81-90/hyland-effectivetopos.pdf lJ.M.E. Hyland 7. Realizability: An Introduction to its Categorical Side https://www.amazon.com/Realizability-152-Introduction-Categorical-Foundations/dp/0444515844 Jaap van Oosten 8. Using the internal language of toposes in algebraic geometry https://arxiv.org/abs/2111.03685 Ingo Blechschmidt 9. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem https://www.ps.uni-saarland.de/Publications/documents/ForsterEtAl\_2018\_On-Synthetic-Undecidability.pdf Yannick Forster,Dominik Kirst, Gert Smolka 10. Synthetic topology of data types and classical spaces https://www.cs.bham.ac.uk/~mhe/papers/barbados.pdf Martın Escardo 11. Foundations of Constructive Mathematics: Metamathematical Studies https://a.co/d/bz4zWUE Michael J. Beeson