-
Cauchy-completions and the rule of unique choice in relational doctrines
Authors:
Francesco Dagnino,
Fabio Pasquali
Abstract:
Lawvere's generalised the notion of complete metric space to the field of enriched categories: an enriched category is said to be Cauchy-complete if every left adjoint bimodule into it is represented by an enriched functor. Looking at this definition from a logical standpoint, regarding bimodules as an abstraction of relations and functors as an abstraction of functions, Cauchy-completeness resemb…
▽ More
Lawvere's generalised the notion of complete metric space to the field of enriched categories: an enriched category is said to be Cauchy-complete if every left adjoint bimodule into it is represented by an enriched functor. Looking at this definition from a logical standpoint, regarding bimodules as an abstraction of relations and functors as an abstraction of functions, Cauchy-completeness resembles a formulation of the rule of unique choice. In this paper, we make this analogy precise, using the language of relational doctrines, a categorical tool that provides a functorial description of the calculus of relations, in the same way Lawvere's hyperdoctrines give a functorial description of predicate logic. Given a relational doctrine, we define Cauchy-complete objects as those objects of the domain category satisfying the rule of unique choice. Then, we present a universal construction that completes a relational doctrine with the rule of unique choice, that is, producing a new relational doctrine where all objects are Cauchy-complete. We also introduce relational doctrines with singleton objects and show that these have the minimal structure needed to build the reflector of the full subcategory of its domain on Cauchy-complete objects. The main result is that this reflector exists if and only if the relational doctrine has singleton objects and this happens if and only if its restriction to Cauchy-complete objects is equivalent to its completion with the rule of unique choice. We support our results with many examples, also falling outside the scope of standard doctrines, such as complete metric spaces, Banach spaces and compact Hausdorff spaces in the general context of monoidal topology, which are all shown to be Cauchy-complete objects for appropriate relational doctrines.
△ Less
Submitted 29 February, 2024;
originally announced February 2024.
-
Quasitoposes as elementary quotient completions
Authors:
Maria Emilia Maietti,
Fabio Pasquali,
Giuseppe Rosolini
Abstract:
The elementary quotient completion of an elementary doctrine in the sense of Lawvere was introduced in previous work by the first and third authors. It generalises the exact completion of a category with finite products and weak equalisers. In this paper we characterise when an elementary quotient completion is a quasi-topos. We obtain as a corollary a complete characterisation of when an elementa…
▽ More
The elementary quotient completion of an elementary doctrine in the sense of Lawvere was introduced in previous work by the first and third authors. It generalises the exact completion of a category with finite products and weak equalisers. In this paper we characterise when an elementary quotient completion is a quasi-topos. We obtain as a corollary a complete characterisation of when an elementary quotient completions is an elementary topos. As a byproduct we determine also when the elementary quotient completion of a tripos is equivalent to the doctrine obtained via the tripos-to-topos construction. Our results are reminiscent of other works regarding exact completions and put those under a common scheme: in particular, Carboni and Vitale's characterisation of exact completions in terms of their projective objects, Carboni and Rosolini's characterisation of locally cartesian closed exact completions, also in the revision by Emmenegger, and Menni's characterisation of the exact completions which are elementary toposes.
△ Less
Submitted 28 December, 2023; v1 submitted 30 November, 2021;
originally announced November 2021.
-
Quantitative Equality in Substructural Logic via Lipschitz Doctrines
Authors:
Francesco Dagnino,
Fabio Pasquali
Abstract:
Substructural logics naturally support a quantitative interpretation of formulas, as they are seen as consumable resources. Distances are the quantitative counterpart of equivalence relations: they measure how much two objects are similar, rather than just saying whether they are equivalent or not. Hence, they provide the natural choice for modelling equality in a substructural setting. In this pa…
▽ More
Substructural logics naturally support a quantitative interpretation of formulas, as they are seen as consumable resources. Distances are the quantitative counterpart of equivalence relations: they measure how much two objects are similar, rather than just saying whether they are equivalent or not. Hence, they provide the natural choice for modelling equality in a substructural setting. In this paper, we develop this idea, using the categorical language of Lawvere's doctrines. We work in a minimal fragment of Linear Logic enriched by graded modalities, which are needed to write a resource sensitive substitution rule for equality, enabling its quantitative interpretation as a distance. We introduce both a deductive calculus and the notion of Lipschitz doctrine to give it a sound and complete categorical semantics. The study of 2-categorical properties of Lipschitz doctrines provides us with a universal construction, which generates examples based for instance on metric spaces and quantitative realisability. Finally, we show how to smoothly extend our results to richer substructural logics, up to full Linear Logic with quantifiers.
△ Less
Submitted 29 April, 2024; v1 submitted 11 October, 2021;
originally announced October 2021.
-
A characterisation of elementary fibrations
Authors:
Jacopo Emmenegger,
Fabio Pasquali,
Giuseppe Rosolini
Abstract:
Grothendieck fibrations provide a unifying algebraic framework that underlies the treatment of various form of logics, such as first order logic, higher order logics and dependent type theories. In the categorical approach to logic proposed by Lawvere, which systematically uses adjoints to describe the logical operations, equality is presented in the form of a left adjoint to reindexing along a di…
▽ More
Grothendieck fibrations provide a unifying algebraic framework that underlies the treatment of various form of logics, such as first order logic, higher order logics and dependent type theories. In the categorical approach to logic proposed by Lawvere, which systematically uses adjoints to describe the logical operations, equality is presented in the form of a left adjoint to reindexing along a diagonal arrows in the base. Taking advantage of the modular perspective provided by category theory, one can look at those Grothendieck fibrations which sustain just the structure of equality, the so-called elementary fibrations, aka fibrations with equality. The present paper provides a characterisation of elementary fibrations based on particular structures in the fibres, called transporters. The characterisation is a substantial generalisation of the one already available for faithful fibrations. There is a close resemblance between transporters and the structures used in the semantics of the identity type of Martin-Löf type theory. We close the paper by comparing the two.
△ Less
Submitted 24 September, 2020; v1 submitted 31 July, 2020;
originally announced July 2020.
-
iProStruct2D: Identifying protein structural classes by deep learning via 2D representations
Authors:
Loris Nanni,
Alessandra Lumini,
Federica Pasquali,
Sheryl Brahnam
Abstract:
In this paper we address the problem of protein classification starting from a multi-view 2D representation of proteins. From each 3D protein structure, a large set of 2D projections is generated using the protein visualization software Jmol. This set of multi-view 2D representations includes 13 different types of protein visualizations that emphasize specific properties of protein structure (e.g.…
▽ More
In this paper we address the problem of protein classification starting from a multi-view 2D representation of proteins. From each 3D protein structure, a large set of 2D projections is generated using the protein visualization software Jmol. This set of multi-view 2D representations includes 13 different types of protein visualizations that emphasize specific properties of protein structure (e.g., a backbone visualization that displays the backbone structure of the protein as a trace of the Cα atom). Each type of representation is used to train a different Convolutional Neural Network (CNN), and the fusion of these CNNs is shown to be able to exploit the diversity of different types of representations to improve classification performance. In addition, several multi-view projections are obtained by uniformly rotating the protein structure around its central X, Y, and Z viewing axes to produce 125 images. This approach can be considered a data augmentation method for improving the performance of the classifier and can be used in both the training and the testing phases. Experimental evaluation of the proposed approach on two datasets demonstrates the strength of the proposed method with respect to the other state-of-the-art approaches. The MATLAB code used in this paper is available at https://github.com/LorisNanni.
△ Less
Submitted 11 June, 2019;
originally announced June 2019.
-
Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies
Authors:
Maria Emilia Maietti,
Fabio Pasquali,
Giuseppe Rosolini
Abstract:
Hyland's effective topos offers an important realizability model for constructive mathematics in the form of a category whose internal logic validates Church's Thesis. It also contains a boolean full sub-quasitopos of "assemblies" where only a restricted form of Church's Thesis survives. In the present paper we compare the effective topos and the quasitopos of assemblies each as the elementary quo…
▽ More
Hyland's effective topos offers an important realizability model for constructive mathematics in the form of a category whose internal logic validates Church's Thesis. It also contains a boolean full sub-quasitopos of "assemblies" where only a restricted form of Church's Thesis survives. In the present paper we compare the effective topos and the quasitopos of assemblies each as the elementary quotient completions of a Lawvere doctrine based on the partitioned assemblies. In that way we can explain why the two forms of Church's Thesis each category satisfies differ by the way each is inherited from specific properties of the doctrine which determines the elementary quotient completion.
△ Less
Submitted 21 June, 2019; v1 submitted 18 February, 2018;
originally announced February 2018.
-
Aristotle's square of opposition in the light of Hilbert's epsilon and tau quantifiers
Authors:
Fabio Pasquali,
Christian Retoré
Abstract:
Aristotle considered particular quantified sentences in his study of syllogisms and in his famous square of opposition. Of course, the logical formulas in Aristotle work were not modern formulas of mathematical logic, but ordinary sentences of natural language. Nowadays natural language sentences are turned into formulas of predicate logic as defined by Frege, but, it is not clear that those Frege…
▽ More
Aristotle considered particular quantified sentences in his study of syllogisms and in his famous square of opposition. Of course, the logical formulas in Aristotle work were not modern formulas of mathematical logic, but ordinary sentences of natural language. Nowadays natural language sentences are turned into formulas of predicate logic as defined by Frege, but, it is not clear that those Fregean sentences are faithful representations of natural language sentences. Indeed, the usual modelling of natural language quantifiers does not fully correspond to natural language syntax, as we shall see. This is the reason why Hilbert's epsilon and tau quantifiers (that go beyond usual quantifiers) have been used to model natural language quantifiers. Here we interpret Aristotle quantified sentences as formulas of Hilbert's epsilon and tau calculus. This yields to two potential squares of opposition and provided a natural condition holds, one of these two squares is actually a square of opposition i.e. satisfies the relations of contrary, contradictory, and subalternation.
△ Less
Submitted 27 June, 2016;
originally announced June 2016.
-
Hilbertian Toposes Epsilon Toposes
Authors:
Fabio Pasquali
Abstract:
We study Hilbert's epsilon calculus and Hilbert's partial epsilon calculus in toposes.
We study Hilbert's epsilon calculus and Hilbert's partial epsilon calculus in toposes.
△ Less
Submitted 2 March, 2016;
originally announced March 2016.
-
The axiom of choice, co-comprehension schema and redundancies in triposes
Authors:
Fabio Pasquali
Abstract:
We study the role of the axiom of choice and co-comprehention in second order encoding of first order predicates logic
We study the role of the axiom of choice and co-comprehention in second order encoding of first order predicates logic
△ Less
Submitted 12 February, 2016;
originally announced February 2016.
-
A tripos based on compact Hausdorff spaces
Authors:
Fabio Pasquali
Abstract:
The category of compact Hausdorff spaces is the base of tripos. As such it can be freely completed to an elementary topos.
The category of compact Hausdorff spaces is the base of tripos. As such it can be freely completed to an elementary topos.
△ Less
Submitted 10 February, 2016;
originally announced February 2016.
-
A categorical semantic for the Typed Epsilon Calculus
Authors:
Fabio Pasquali
Abstract:
We show that every boolean category satisfying AC provides a categorical semantic of the typed Epsilon calculus.
We show that every boolean category satisfying AC provides a categorical semantic of the typed Epsilon calculus.
△ Less
Submitted 8 September, 2014;
originally announced September 2014.
-
Remarks on the Tripos To Topos Construction: extensionality, comprehensions, quotients and cauchy-complete objects
Authors:
Fabio Pasquali
Abstract:
We give a description of the Tripos To Topos construction in terms of four free constructions. We prove that these compose up to give a free construction from the category of triposes and logical morphisms to the category of toposes and logical functors. Then we show that other similar constructions, i.e. the one given by Frey in \cite{frey} and that of Carboni in \cite{carbons} are instances of t…
▽ More
We give a description of the Tripos To Topos construction in terms of four free constructions. We prove that these compose up to give a free construction from the category of triposes and logical morphisms to the category of toposes and logical functors. Then we show that other similar constructions, i.e. the one given by Frey in \cite{frey} and that of Carboni in \cite{carbons} are instances of this one.
△ Less
Submitted 24 February, 2014; v1 submitted 30 January, 2014;
originally announced January 2014.
-
A sheafification theorem for doctrines
Authors:
Fabio Pasquali
Abstract:
We define the notion of sheaf in the context of doctrines. We prove the associate sheaf functor theorem. We show that grothendieck toposes and toposes obtained by the tripos to topos construction are instances of categories of sheaves for a suitable doctrine.
We define the notion of sheaf in the context of doctrines. We prove the associate sheaf functor theorem. We show that grothendieck toposes and toposes obtained by the tripos to topos construction are instances of categories of sheaves for a suitable doctrine.
△ Less
Submitted 4 September, 2014; v1 submitted 6 November, 2013;
originally announced November 2013.
-
A co-free construction for elementary doctrines
Authors:
Fabio Pasquali
Abstract:
We provide a co-free construction which adds elementary structure to a primary doctrine. We show that the construction preserves comprehensions and all the logical operations which are in the starting doctrine, in the sense that it maps a first order many-sorted theory into a the same theory formulated with equality. As a corollary it forces an implicational doctrine to have an extentional entailm…
▽ More
We provide a co-free construction which adds elementary structure to a primary doctrine. We show that the construction preserves comprehensions and all the logical operations which are in the starting doctrine, in the sense that it maps a first order many-sorted theory into a the same theory formulated with equality. As a corollary it forces an implicational doctrine to have an extentional entailment.
△ Less
Submitted 30 January, 2014; v1 submitted 8 November, 2012;
originally announced November 2012.
