Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: our papers

Topic: Machine Space I: Weak exponentials and quantification ove...

Peter Faul (Sep 29 2022 at 13:42):

@Graham Manuell and I have just put out a preprint formalizing some aspects related to the semidecdiable/verifiable interpretation of topology.

https://arxiv.org/abs/2209.11339

If you've ever been curious about this logical reinterpretation of topology give our paper a look as it offers a fairly gentle introduction to the ideas. As a taster of some of the cooler facts relating to this observation, given a compact set $K$ and a verifiable Property $P$, you can semidecide whether every member of $K$ satisfies $P$, even when $K$ is infinite! This is even implementable on a computer as Escardo showed with his seemingly impossible function program universally quantifying over Cantor Space.

As to the results in our paper, they were motivated by two unrelated questions:

1. From the perspective of verifiability can we understand why exponentials do not always exist for spaces.
2. To what extent is there a uniform, purely topological, procedure for universally quantifying over compact spaces.

In answering these questions we distinguish between verifiable properties themselves and processes that actually carry out the verification procedure, the former being opens and the latter being what we term machines. These machines can be formalized using frame presentations, where each generator is interpreted as a basic machine.

We show that for every space with a presentation there is a canonical weak exponential which we term machine space, with evaluation map taking in a point and a machine and determining whether the machine accepts the point or not. The existence of this space can be justified entirely from first principles, which then makes our consequent derivation of spaces of opens for locally compact spaces from machine space philosophically satisfying (at least to our minds).

Using the formalism of machine space we are then also able to describe an algorithm on compact space $K$ which takes in a machine and halts precisely if each point in $K$ is accepted by the machine. Our approach can be related to the more domain theoretic approaches of Escardo as we describe in the last section.

Jean-Baptiste Vienney (Sep 30 2022 at 00:35):

Thank you, it looks fascinating! All I knew about topology and logic is that the set of subsets of a set is a Boolean algebra and I was wondering what we can do we that. Now I can read your paper to know much more!

Peter Faul (Oct 01 2022 at 13:18):

I hope you like it! Let me know if you have any questions!