Giulia Battilotti

We introduce the notion of infinitary preorder and use it to obtain a predicative presentation of sup-lattices by generators and relations. The method is uniform in that it extends in a modular way to obtain a presentation of quantales, as “sup-lattices on monoids”, by using the notion of pretopology.Our presentation is then applied to frames, the link with Johnstone’s presentation of frames is spelled out, and his theorem on freely generated frames becomes a special case of our results on quantales.The main motivation of this paper is to contribute to the development of formal topology. That is why all our definitions and proofs can be expressed within an intuitionistic and predicative foundation, like constructive type theory.

We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection. To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube.

In the present paper we give the first proof-theoretical example of an embedding of classical logic into a quantum-like logic. This is performed in the framework of basic logic, where a proof-theoretical approach to quantum logic is convenient. We consider basic orthologic, that corresponds to a sequential formulation of paraconsistent quantum logic, and which is given by basic orthologic added with weakening and contraction, in a language with Girard's negation. In the paper we first consider a convenient cut-free calculus for classical logic, in the same language; then, in a language enriched with a new kind of literals, we introduce basic orthologic with a primitive modality, where classical logic is embeddable. Similarly to Girard's negation, our modality is not a connective but conceivable as an operator defined inductively on the set of formulae. This allows us to obtain a calculus which enjoys cut-elimination.

We introduce a sequent calculusBfor a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic. quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterizeBpositively: reflection, symmetry and visibility.A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection.To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube.