16:00
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.