Equideductive categories and their logic

"Equideductive categories and their logic" www.PaulTaylor.EU/ASD/extension Under the heading "Locally cartesian closed categories", on 8 October 2007, I asked whether anybody had investigated to what extent the true statement but an incorrect definition

Any topos is a CCC with an internal Heyting algebra, actually gives rise to interesting structure. However, I didn't get much response.

I went on

Suppose that the category has all FINITE LIMITS (terminal object, finite products and equalisers) and POWERS Sigma^X of an internal DISTRIBUTIVE LATTICE (Sigma, top, bot, meet, join). Maybe there is also a natural numbers object N and joins Sigma^N->Sigma with the Frobenius law. (I would also like this to obey the monadic and Phoa principles of ASD, but I'm not going to spell them out here.)

Maps X->Sigma give rise to a "geometric logic" of "open" subspaces.

Then the order relation between maps X->Sigma^Y leads to a richer logic of "general" subspaces, with => and forall_Y.

A logical formula of the more general form consists of geometric sub-formulae joined together with => and forall, to which we might add the other first order connectives as "syntactic sugar", defined in the usual classical way. If a geometric sub-formula is immediately enclosed in forall_K or exists_N, where K happens to be compact or N overt, then this a priori more general quantifier may be considered to be part of the geometric sub-formula.

The draft paper advertised above investigates these ideas. This work was part of a re-formulation of Dana Scott's equilogical space construction about which you can find three sets of slides at www.PaulTaylor.EU/slides/ and the details will follow shortly. My lengthy posting on "Applications of the Yoneda embedding" on 20 June 2009 also provides background material for this. However, it has turned out to be very fruitful to leave the CCC aside and first consider the properties of a category that "lies nicely" within its cartesian closed extensions. The categories of sets, of sober topological spaces (in the textbook sense) and of affine varieties have the appropriate properties. However, because of the counterexample that I gave in "Aspects of locale theory" on 9 June 2009, the category of locales does not (products do not preserve epis). As I suggested in 2007, the key idea is to study equalisers targeted at exponentials. In terms of the Yoneda embedding, if we have a pair of maps from a representable presheaf to the exponential (Sigma^-) of another representable, is the equaliser representable too? We can reformulate this in the original category, without using presheaves, as a (kind of) PARTIAL PRODUCT. The categories of sets, topological spaces and affine varieties have these partial products. (I would like to thank Andrea Schalk, Mike Barr and possibly Robin Cockett for joining me in banging our heads against the brick wall of trying to find out whether locales have them too. Probably they don't, but I'm not sure whether it is this or something else that goes wrong.) An EQUIDEDUCTIVE CATEGORY is one that has finite limits, (my) partial products, an object Sigma that is injective wrt the monos that arise from partial products, and enough injectives. It turns out that those objects A that have exponentials Sigma^A are SOBER in my abstract sense, and the adjunction Sigma^- -| Sigma^- on this subcategory is monadic. In other words we have the characteristic properties of the subcategory of locally compact spaces within the category of sober topological spaces, without assuming any structure on Sigma such as being a lattice. EQUIDEDUCTIVE LOGIC captures this categorical structure in symbolic form. It is a predicate calculus whose object language is the sober lambda calculus. The chief feature is a quantified implication that justifies the (recursive) notation E = { x:A | All y:B. q(y) => fxy=gxy } for the equaliser E >--> A ====> Sigma^Y where Y = {b:B | q(y)}. Note that the predicates that are defined by this logic are general subobjects, not terms of type Sigma^A. Using quantification over terms of type Sigma^A, one can define an "existential quantifier". This is the most striking aspect of equideductive logic: although this is an old idea (maybe due to Russell) from higher order logic, it turns out to characterise the EPIs in the category, which have to be preserved by products. Of course, epis need not be surjective. For example N-->>X is epi amongst sober spaces, where X is the domain of ascending natural numbers, with T=oo. This means that one has to be EXTREMELY careful in using this quantifier -- it only has a restricted Frobenius law and doesn't allow substitution -- but I think that it will turn out to be very useful. For example, Scott continuity can be expressed in the form that, for phi:Sigma^N, "there exists" a finite set S such that phi n <=> n in S. What this means is that it is sufficient to test this case when proving equality of terms of type Sigma. We recover topology (in the style of ASD) by requiring SOME of these quantifiers to agree with structure on Sigma. That is, a space {x:A|p(x)} is compact or overt if the PREDICATE given by quantification of a term of type Sigma^A agreed with another term of type Sigma. On the other hand, and coming back to the question at the top of this posting, we recover set theory (ie an elementary topos) by requiring ALL quantifiers to agree with operators on Sigma. I trust that I will not hear any further repetition of the claim that ASD is restricted to locally compact spaces. This paper essentially replaces "Subspaces in ASD" and the monadic lambda calculus. It also fills in several gaps in other papers, such as allowing equational hypotheses and constructing the compact and overt subspaces that are described by modal operators. Paul Taylor [For admin and other information see: http://www.mta.ca/~cat-dist/ ]