|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 listsBabbage Seminar Series Paediatric Endocrinology & Diabetes Postgraduate Seminar series Study Group on a Langlands Correspondence for Loop Groups
Other talksTear analysis in dogs: a quick, non-invasive, overlooked diagnostic tool Security and Privacy in Machine Learning Annual Conversazione: Cambridge’s oldest celebration of citizen science! Bridging Integrator 1 (BIN1) a major player in the ultrastructure dependent pathophysiology of heart failure? Evaluation of 3C technology for detection of AMR gene transfer in E. coli Masterclass: Crystal growth kinetics