|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Equideductive logic and CCCs with subspaces
If you have a question about this talk, please contact Sam Staton.
NOTE UNUSUAL DAY.
In any cartesian closed category with equalisers, the logic of regular monos (maps that arise as equalisers) of course has conjunctions. But also, if p(x) represents a regular mono into X and f,g: X x Y—> Z are any maps then there is a regular mono into Y represented by q(y) = All x. p(x) ==> f(x,y) = g(x,y). Categorically, q(y) can be defined by a kind of partial product.
This apparently rather feeble logic is nevertheless interesting for a number of reasons:
It is how we reason with proofs of equations in algebra, ie treating judgements that one equation follows from others, proof rules about such judgements (such as induction schemes), etc., as arbitrarily nestable implications.
It may be interpreted in the category of sober topological spaces, and maybe locales.
Together with the lattice structure on the Sierpinski space and an axiom that identifies equideductive implication with the lattice order, it is the logic that is needed to form open, closed, compact and overt subspaces in ASD .
It provides the abstract (type-theoretic) basis on which to construct a cartesian closed category with equalisers similar to Scott’s equilogical spaces.
However, the logical formulae that are generated when working with it get complicated, and seem to need another simplifying axiom, for which I have a candidate. This raises the issue of consistency, but the weakness of equideductive logic is its strength: it has a realisability interpretion in itself, which ought to provide a tool for proving conservativity of extensions, but I need some help to do this.
More on abstract stone duality at Paul’s web page: www.PaulTaylor.EU/ASD .
The slides are at PaulTaylor.EU/slides/#09-Cambridge .
This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsDevelopmental Biology Seminar Series Seminars on Adaptation to Climate Change Proteins, Genomes & Computers
Other talksMolecular dissection approaches to study diseased tissues Use of grass seed resources c. 31 ka by modern humans at the Haua Fteah cave, northeast Libya 'Partisanship, petitioning, and deliberation in British politics, c. 1689-1750' The SHIP Experiment The textualist orthodoxy of the Victorian treatise on statute law Lorenz chaos beyond the attractor