Continuity via Logic

20 January 2016
Steve Vickers

Point-free topology can often seem like an algebraic almost-topology, 
> not quite the same but still interesting to those with an interest in 
> it. There is also a tradition of it in computer science, traceable back 
> to Scott's topological model of the untyped lambda-calculus, and 
> developing through Abramsky's 1987 thesis. There the point-free approach 
> can be seen as giving new insights (from a logic of observations), 
> albeit in a context where it is equivalent to point-set topology. It was 
> in that tradition that I wrote my own book "Topology via Logic".
> Absent from my book, however, was a rather deeper connection with logic 
> that was already known from topos theory: if one respects certain 
> logical constraints (of geometric logic), then the maps one constructs 
> are automatically continuous. Given a generic point x of X, if one 
> geometrically constructs a point of Y, then one has constructed a 
> continuous map from X to Y. This is in fact a point-free result, even 
> though it unashamedly uses points.
> This "continuity via logic", continuity as geometricity, takes one 
> rather further than simple continuity of maps. Sheaves and bundles can 
> be understood as continuous set-valued or space-valued maps, and topos 
> theory makes this meaningful - with the proviso that, to make it run 
> cleanly, all spaces have to be point-free. In the resulting fibrewise 
> topology via logic, every geometric construction of spaces (example: 
> point-free hyperspaces, or powerlocales) leads automatically to a 
> fibrewise construction on bundles.
> I shall present an overview of this framework, as well as touching on 
> recent work using Joyal's Arithmetic Universes. This bears on the logic 
> itself, and aims to replace the geometric logic, with its infinitary 
> disjunctions, by a finitary "arithmetic type theory" that still has the 
> intrinsic continuity, and is strong enough to encompass significant 
> amounts of real analysis.

  • Analytic Topology in Mathematics and Computer Science