PDF (821 kb) DVI (423 kb) PostScript (compressed) (650 kb) A5 PS booklet (compressed) (651 kb) What are these? [22 Aug 2013] | This first paper studies the interaction between equalisers and exponentials. Categorically, such subspaces are characterised as "partial products". The logic is a kind of predicate calculus with ∀, ⇒ and & whose object language is the sober λ-calculus. The equivalence between these two formulations is proved. Although there is a special object Σ, no structure is yet assumed for it. This work is intended as an alternative to Subspaces in ASD for the foundations that are needed for the applications of ASD. |
PDF (294 kb) DVI (132 kb) PostScript (compressed) (162 kb) A5 PS booklet (compressed) (155 kb) What are these? [13 Jan 2011] | Although the logic is only defined to have universal quantification, conjunction and equality, it is possible to define an existential quantifier too. This quantifier agrees with the epis in an equideductive category, which form a factorisation system together with the partial product inclusions. The epis are preserved by products but not by general pullbacks, corresponding to the fact that the rules for the quantifier are subject to severe limitations on the use of variables and in particular do not allow substitution. Such a category also has stable disjoint coproducts. The only structure that is assumed on Σ for this is a single constant ∗. This paper begins with a rapid survey of the many different meaning that have been given to the existential quantifier in various forms of symbolic and categorical logic. I would appreciate comments on this historical material as well as on the main subject matter of the paper. |
PDF (285 kb) DVI (121 kb) PostScript (compressed) (141 kb) A5 PS booklet (compressed) (133 kb) What are these? [20 Feb 2011] | This is the first paper in the equideductive programme that assumes a lattice structure on Σ. It begins from the question of when Σ is a dominance, i.e. it classifies some class of "open" inclusions. This question leads to an "internal" logic of open subspaces. Discrete, compact, overt and Hausdorff spaces are those form which the external (in)equality or quantifier is represented by a lambda term. We develop these ideas into a new, two-level, logical calculus for open and general subspaces in computable general topology. The two levels coincide, i.e. the external logic is always represented by internal structure on Σ ≡ Ω, iff the category is a topos. |
This is www.PaulTaylor.EU/ASD/equideductive.php and it was derived from ASD/equideductive.tex which was last modified on 20 February 2011.