Point-free real analysis - new paper

[Steven Vickers <s.j.vickers.1@bham.ac.uk>]

[-- Attachment #1: Type: text/plain, Size: 1678 bytes --]

Can real analysis be done point-free, for locales? That would be daunting to attempt in terms of frames and frame homomorphisms, but it has long been understood that an alternative is to use points and reason geometrically so that one is not just working with the global points (which may be insufficient).


My student Ming Ng developed real exponentiation and logarithms in this style. I have now arXived a paper (arXiv:2312.05228) that shows how to differentiate them. It relies on first proving the Fundamental Theorem of Calculus, after which the development is more or less conventional.


The style is quite natural, and reminiscent of Bishop’s constructive reasoning, though with a different mathematical trajectory. However, it is still an open question whether it is truly constructive in the sense of extracting algorithms from proofs. I have some notes on this, formatted as slides, at


  https://www.cs.bham.ac.uk/~sjv/GeologConsSlides.pdf<https://protect-au.mimecast.com/s/V7i_CgZ05Jf79Y78INW0HG?domain=cs.bham.ac.uk>


Steve Vickers.



You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message.

View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 5682 bytes --]