The categorified theories known as “doctrines” specify a category equipped with extra structure, analogous to how ordinary theories specify a set with extra structure. We introduce a new framework ...for doctrines based on double category theory. A cartesian double theory is defined to be a small double category with finite products and a model of a cartesian double theory to be a finite product-preserving lax functor out of it. Many familiar categorical structures are models of cartesian double theories, including categories, presheaves, monoidal categories, braided and symmetric monoidal categories, 2-groups, multicategories, and cartesian and cocartesian categories. We show that every cartesian double theory has a unital virtual double category of models, with lax maps between models given by cartesian lax natural transformations, bimodules between models given by cartesian modules, and multicells given by multimodulations. In many cases, the virtual double category of models is representable, hence is a genuine double category. Moreover, when restricted to pseudo maps, every cartesian double theory has a virtual equipment of models, hence an equipment of models in the representable case. Compared with 2-monads, double theories have the advantage of being straightforwardly presentable by generators and relations, as we illustrate through a large number of examples.
It is well-known that the construction of Zariski spectra of (commutative) rings yields a dual adjunction between the category of rings and the category of locally ringed spaces. There are many ...constructions of spectra of algebras in various contexts giving such adjunctions. Michel Coste unified them in the language of categorical logic by showing that, for an appropriate triple (T0,T,Λ) (which we call a spatial Coste context), each T0-model can be associated with a T-modelled space and that this yields a dual adjunction between the category of T0-models and the category of T-modelled spaces and “admissible” morphisms. However, most of his proofs remain unpublished. In this paper, we introduce an alternative construction of spectra of T0-models, which is reminiscent of Zariski spectra, and give a new proof of Coste adjunction. Moreover, we also extend spectra of T0-models to relative spectra of T0-modelled spaces and prove the existence of limits and colimits in the involved categories of modelled spaces. We can deduce, for instance, that the category of ringed spaces whose stalks are fields is complete and cocomplete.
We determine sufficient structure for an elementary topos to emulate Nelson's Internal Set Theory in its internal language, and show that any topos satisfying the internal axiom of choice occurs as a ...universe of standard objects and maps. This development allows one to employ the proof methods of nonstandard analysis (transfer, standardisation, and idealisation) in new environments such as toposes of G-sets and Boolean étendues.
Abstract In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using ...inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic raises some technical and conceptual issues. We relate Sandqvist’s (complete) base-extension semantics of intuitionistic propositional logic to categorical proof theory in presheaves, reconstructing categorically the soundness and completeness arguments, thereby demonstrating the naturality of Sandqvist’s constructions. This naturality includes Sandqvist’s treatment of disjunction that is based on its second-order or elimination-rule presentation. These constructions embody not just validity, but certain forms of objects of justifications. This analysis is taken a step further by showing that from the perspective of validity, Sandqvist’s semantics can also be viewed as the natural disjunction in a category of sheaves.
We extend Lawvere-Pitts prop-categories (aka. hyperdoctrines) to develop a general framework for providing fibered algebraic semantics for general first-order logics. This framework includes a ...natural notion of substitution, which allows first-order logics to be considered as structural closure operators just as propositional logics are in abstract algebraic logic. We then establish an extension of the homomorphism theorem from universal algebra for generalized prop-categories and characterize two natural closure operators on the prop-categorical semantics. The first closes a class of structures (which are interpreted as morphisms of prop-categories) under the satisfaction of their common first-order theory and the second closes a class of prop-categories under their associated first-order consequence. It turns out that these closure operators have characterizations that closely mirror Birkhoff's characterization of the closure of a class of algebras under the satisfaction of their common equational theory and Blok and Jónsson's characterization of closure under equational consequence, respectively. These algebraic characterizations of the first-order closure operators are unique to the prop-categorical semantics. They do not have analogues, for example, in the Tarskian semantics for classical first-order logic. The prop-categories we consider are much more general than traditional intuitionistic prop-categories or triposes (i.e., topos representing indexed partially ordered sets). Nonetheless, to the best of our knowledge, our results are new, even when restricted to these special classes of prop-categories.
Abstract
We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model-theoretic constructions underlying forcing and realizability (both in ...intuitionistic and classical logic). The salient feature of this structure is that its elements can be seen both as truth values and as (generalized) realizers, thus blurring the frontier between proofs and types. We show that each implicative algebra induces a (
Set
-based) tripos, using a construction that is reminiscent from the construction of a realizability tripos from a partial combinatory algebra. Relating this construction with the corresponding constructions in forcing and realizability, we conclude that the class of implicative triposes encompasses all forcing triposes (both intuitionistic and classical), all classical realizability triposes (in the sense of Krivine), and all intuitionistic realizability triposes built from partial combinatory algebras.
What should a generic object be? Sterling, Jonathan
Mathematical structures in computer science,
01/2023, Volume:
33, Issue:
1
Journal Article
Peer reviewed
Open access
Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of (split) generic objects, Jacobs develops a menagerie of important ...fibrational structures with applications to categorical logic and computer science, including higher order fibrations, polymorphic fibrations,
$\lambda2$
-fibrations, triposes, and others. We observe that a split generic object need not in particular be a generic object under the given definitions, and that the definitions of polymorphic fibrations, triposes, etc. are strict enough to rule out some fundamental examples: for instance, the fibered preorder induced by a partial combinatory algebra in realizability is not a tripos in this sense. We propose a new alignment of terminology that emphasizes the forms of generic object appearing most commonly in nature, i.e. in the study of internal categories, triposes, and the denotational semantics of polymorphism. In addition, we propose a new class of acyclic generic objects inspired by recent developments in higher category theory and the semantics of homotopy type theory, generalizing the realignment property of universes to the setting of an arbitrary fibration.
We prove that the category
$\mathsf {SBor}$
of standard Borel spaces is the (bi-)initial object in the 2-category of countably complete Boolean (countably) extensive categories. This means that
...$\mathsf {SBor}$
is the universal category admitting some familiar algebraic operations of countable arity (e.g., countable products and unions) obeying some simple compatibility conditions (e.g., products distribute over disjoint unions). More generally, for any infinite regular cardinal
$\kappa $
, the dual of the category
$\kappa \mathsf {Bool}_{\kappa }$
of
$\kappa $
-presented
$\kappa $
-complete Boolean algebras is (bi-)initial in the 2-category of
$\kappa $
-complete Boolean (
$\kappa $
-)extensive categories.
PDF
