categories - Category Theory list
 help / color / mirror / Atom feed
* Point-free real analysis - new paper
@ 2023-12-11 18:11 Steven Vickers
  0 siblings, 0 replies; only message in thread
From: Steven Vickers @ 2023-12-11 18:11 UTC (permalink / raw)
  To: Categories

[-- 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<>

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<>   |   Leave group<>   |   Learn more about Microsoft 365 Groups<>

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

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2023-12-11 22:12 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-12-11 18:11 Point-free real analysis - new paper Steven Vickers

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).