1.  3
    Categorical Logic and Type Theory.Bart Jacobs - 2000 - Bulletin of Symbolic Logic 6 (2):225-229.
    Direct download  
    Export citation  
    Bookmark   10 citations  
  2.  38
    Dagger Categories of Tame Relations.Bart Jacobs - 2013 - Logica Universalis 7 (3):341-370.
    Within the context of an involutive monoidal category the notion of a comparison relation ${\mathsf{cp} : \overline{X} \otimes X \rightarrow \Omega}$ is identified. Instances are equality = on sets, inequality ${\leq}$ on posets, orthogonality ${\perp}$ on orthomodular lattices, non-empty intersection on powersets, and inner product ${\langle {-}|{-} \rangle}$ on vector or Hilbert spaces. Associated with a collection of such (symmetric) comparison relations a dagger category is defined with “tame” relations as morphisms. Examples include familiar categories in the foundations of quantum (...)
    Direct download (10 more)  
    Export citation  
    Bookmark   1 citation  
  3.  18
    Involutive Categories and Monoids, with a GNS-Correspondence.Bart Jacobs - 2012 - Foundations of Physics 42 (7):874-895.
    This paper develops the basics of the theory of involutive categories and shows that such categories provide the natural setting in which to describe involutive monoids. It is shown how categories of Eilenberg-Moore algebras of involutive monads are involutive, with conjugation for modules and vector spaces as special case. A part of the so-called Gelfand–Naimark–Segal (GNS) construction is identified as an isomorphism of categories, relating states on involutive monoids and inner products. This correspondence exists in arbritrary involutive symmetric monoidal categories.
    Direct download (11 more)  
    Export citation  
    Bookmark   1 citation  
  4.  35
    The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
    Martin-Löf's constructive type theory forms the basis of this paper. His central notions of category and set, and their relations with Russell's type theories, are discussed. It is shown that addition of an axiom - treating the category of propositions as a set and thereby enabling higher order quantification - leads to inconsistency. This theorem is a variant of Girard's paradox, which is a translation into type theory of Mirimanoff's paradox (concerning the set of all well-founded sets). The occurrence of (...)
    Direct download (5 more)  
    Export citation  
    Bookmark   3 citations  
  5.  11
    Semantics of Weakening and Contraction.Bart Jacobs - 1994 - Annals of Pure and Applied Logic 69 (1):73-106.
    The shriek modality \s! of linear logic performs two tasks: it restores in annotated from both weakening and contraction. We separate these tasks by introducing two modalities: for weakening and for contraction. These give rise to two logics which are “inbetween” linear and intuitionistic logic: in affine logic one always has a weakening and a for contraction and in relevant logic one always has a contraction and a weakening. The semantics of these logics is obtained from special kinds of monads, (...)
    Direct download (4 more)  
    Export citation  
    Bookmark   2 citations  
  6.  13
    Coreflections in Algebraic Quantum Logic.Bart Jacobs & Jorik Mandemaker - 2012 - Foundations of Physics 42 (7):932-958.
    Various generalizations of Boolean algebras are being studied in algebraic quantum logic, including orthomodular lattices, orthomodular po-sets, orthoalgebras and effect algebras. This paper contains a systematic study of the structure in and between categories of such algebras. It does so via a combination of totalization (of partially defined operations) and transfer of structure via coreflections.
    Direct download (8 more)  
    Export citation