"Real analysis via logic"
Talk 7 September 2024 for
British Logic Colloquium BLC24, Birmingham University.
My recent work with Ming Ng has started to investigate real analysis in a point-free style, suited to topos theory.
I explain how much of this can be explained as logical phenomena.
The space of real numbers is described as a logical theory (for geometric logic), for which real numbers are the models; continuous maps are described by constructions that respect the constraints of geometric logic.
I shall briefly introduce some examples by which logical constructions provide techniques that are less common in the usual development, or even impossible there.
"The Fundamental Theorem of Calculus, point-free"
Talk 30 May 2024 for
Topos Institute Colloquium.
Without going too deeply into the underlying topos theory, I first give a short account of what point-free topology is, how it's done using geometric reasoning, and why one might bother.
I then present as an example the Fundamental Theorem of Calculus (that differentiation is the inverse of integration) and an application to differentiating logs. This is an important step in point-free real analysis, and relates strongly to the work initiated in Ming Ng's thesis. It also illustrates some characteristic features of point-free reasoning, such as a focus on one-side reals and a use of hyperspaces and related constructions.
"Is geometric logic constructive?"
Talk January 2024 at
Dagstuhl Seminar 24021, "From proofs to computation in geometric logic and generalizations".
"Constructive" is in the strict sense, where "there exists" means "we can construct".
I discuss various aspects of the question, and how it might be answered.
"Dependent type theory of point-free topological spaces"
Talk May 2023 for Type theory, constructive mathematics and geometric logic, CIRM, Marseille.
It explains why point-free topology contains a hidden dependent type theory waiting to get out.
"Arithmetic universes: Home of free algebras"
Invited talk Nov 2020 for Erik Palmgren memorial conference, Stockholm.
It outlines my joint paper with Erik Palmgren,
and explains
(I) how AUs hit sweet spot for the Initial Model Theorem;
(II) the algebraic approach to classifying categories that is suggested there;
and (III) how the AU-logic potentially provides foundations for continuous mathematics.
"The interval object [-1, 1]" (given Sep 2017 for Department of Mathematics, Padova University) - outlines The localic compact interval is an Escardó-Simpson interval object; also comments on localic surjections.
TACL talks 2017
The first four of these talks were given 22-23 June 2017 at the TACL summer school, Olomouc, Czech Republic. Their overall title is "ACLT: Algebra, Categories, Logic in Topology - Grothendieck's generalized topological spaces (toposes)". They survey how the ACL disciplines come together to provide the mathematics of generalized spaces, but at the same time get modified in various ways that might be unexpected to mainstream ACL practitioners.
The fifth TACL talk was an invited presentation given 28 June 2017 at the TACL workshop the following week in Prague.
"Arithmetic universes as generalized point-free spaces" (given 17 Apr 2017 for Japan Advanced Institute for Science and Technology and 19 Apr 2017 for Kyoto University) - describes the background for Grothendieck toposes as generalized topological spaces, and how that leads into the recent work with arithmetic universes.
"Grothendieck toposes fibred over elementary toposes" (given 13 Feb 2017 for YaMCATS - Yorkshire and Midlands Category Theory Seminar, University of Leicester) - describes the way that Arithmetic universes and classifying toposes proves base-independent results about classifying toposes, by fibring over a 2-category of elementary toposes.
"Arithmetic universes and type theory" (given 9 Feb 2017 at the University of Padova) - discusses two levels at which Sketches for arithmetic universes suggests connections between arithmetic universes and dependent type theory.
"Sketches for arithmetic universes" (given 21 Oct 2016 for OASIS - Oxford Advanced Seminar for Informatic Structures, Department of Computer Science, University of Oxford) - presents the paper with the same name.
"Coherence for geometricity - BMC" (given 31 March 2015 at the British Mathematics Colloquium, Cambridge; and "Coherence for geometricity - 5WFTop" (given 8 June 2015 at the 5th Workshop on Formal Topology, Institut Mittag-Leffler, Stockholm - These two different talks on the same topic describe a technique forproving coherence of constructive constructions on locales, by reducing from toposes to arithmetic universes.
"Spectral bundles as fibrations and opfibrations" (given 14 December 2012 at the 1st Workshop on Quantum Toposophy, Radbout University Nijmegen) - explains how the contrasting "contravariant" and "covariant" topos approaches to quantum theory can be understood more generally in a bundle picture using opfibrations and fibrations, and presents a general result showing that both classes are preserved by geometric constructions such as the valuation locale (a point-free topological analogue of the Giry monad). Video by the Oxford Quantum Talks Archive.
This three-part tutorial on "Formal Topology and Geomeric Logic" was presented at the 4th Workshop on Formal Topology, Ljubljana, June 2012.
It develops the idea, originating in Grothendieck's work, that continuity in a greatly generalized sense can be understood as adherence to principles of geometricity.
"Bundles" (video by the Oxford Quantum Talks Archive; talk given at the Bellairs McGill-Oxford Workshop on Quantum and Classical Information Flow, Bellairs, 9-14th April 2011) - explains how the idea of bundle can be used to introduce toposes (sheaves as fibrewise discrete bundles), and how geometricity is a general condition for reasoning to work fibrewise; relates these ideas to topos approaches to quantum foundations.
"The fibrewise Vietoris hyperspace" (given 13 December 2010 at the Workshop on Modal Logic and Stone Duality, Amsterdam) - explains how the Vietoris powerlocale can be generalized to a construction fibrewise on localic bundles, and how it relies on the constructivity (topos-valid + geometric) of the Vietoris powerlocale: thus constructive reasoning has a classical payoff.
"Arithmetic universes as generalized spaces" (given 27 November 2010 at the Peripatetic Seminar on Sheaves and Logic PSSL91, Amsterdam) - a presentation of the ideas in "An induction principle for consequence in arithmetic universes". An earlier presentation, "Surviving without function types: Life in an arithmetic universe" was given 22 June 2010 at the International Category Theory Conference CT2010, Genova.
"Aspects of geometric logic" (given 12 November 2010 at the Workshop on Logic, Categories and Semantics, Bordeaux) - gives a broad survey of geometric logic and its unique selling points. Written up as "Continuity is Geometricity".
"Points in geometric point-free topology" (given 6 September 2010 at the Workshop on Constructive Topology, Palermo) - explains how geometricity makes it possible to reason validly about point-free spaces in terms of their points.
"Quantum Topos Theory (given 28 March - 1 April 2010 at the Midland Graduate School in Foundations of Computer Science) - a series of 4 lectures with exercise classes to give a conceptual overview of toposes, quantum theory and the topos approach to quantum theory.
"Geometricity" (given 3rd December 2009 at the Department of Computing, Imperial College) - outlines how geometricity relates to fibrewise point-free topology.
"The Topos Approach in the Qubit Case" (given 18th December 2008 at the 3rd QNET Workshop, Edinburgh) - outlines how the topos approach to quantum mechanics (Imperial, Nijmegen) might be varied to take into account the topology on the space of classical contexts, with illustration from the qubit case.
"Aspects of Topology" (Departmental Seminar, School of Computer Science, University of Brimingham) - Introduces topology and some of its application in theoretical computer science in the "point-free" form, and then leads on to toposes and a novel use (Imperial, Nijmegen) in the formulation of quantum mechanics.
"On the Trail of the Formal Topos" - Advances in Constructive Topology and Logical Foundations, Padua 8-11 October 2008. Discusses routes for extracting predicative content from topos theory.
"Locales via Bundles" - Sheaves in Geometry and Quantum Theory, Nijmegen 3-5 Spetember 2008; slightly briefer version (video by the Oxford Quantum Talks Archive) given at Categories, Logic and Physics, Oxford, 23-24 August 2008. Introduces locales through the idea of bundles, with reference to the topos approaches to quantum theory.
"Fuzzy Sets and Geometric Logic" - 29th Linz Seminar on Fuzzy Set Theory: Foundations of Lattice-Valued Mathematics with Applications to Algebra and Topology, Linz 12-16 February 2008. Explains sheaf accounts of fuzzy sets in terms of geometric logic.
"Schemas as Toposes" - Open University on 2nd July 2002.
Also, some research seminars I gave in 2003-4 (primarily for PhD students) on Category Theory and "Topology via Logic".
Category Theory: comprises lectures I gave at Imperial introducing categories as part of an MSc module on Mathematical Structures for Computer Science.
On my book Topology via Logic: In many ways the lectures followed the book, but they went beyond it in bringing out the deep relationship with constructive logic. Here are the slides: