ABSTRACT. Link to abstract

ABSTRACT. We propose a preliminary study of (in)consistency opera- tors on quasi-Nelson algebras, a variety that generalizes both Nelson and Heyting algebras; our aim us it pave the way for introducing logics of for- mal inconsistency (LFI) in a non-necessarily involutive setting. We show how several results that have been obtained for LFI based on distributive involutive residuated lattices can be extended to quasi-Nelson algebras and their logic. We prove that the classes of algebras thus obtained are equationally axiomatizable, and provide a twist representation for them. Having obtained some insight on filters and congruences, we character- ize the directly indecomposable members of these varieties, showing in particular that two of them are semisimple. Further logical developments and extensions of the present approach are also discussed.

ABSTRACT. This paper extends correspondence theory to the framework of K-algebras, i.e. vector spaces endowed with a bilinear operation, seen as 'Kripke frames'.

For every K-algebra, the lattice of its subspaces can be endowed with the structure of a complete (non necessarily monoidal) residuated lattice. Hence, a sequent of the logic of residuated non-monoidal lattices can be interpreted as a property of its lattice of subspaces.

Thus, correspondence theory can be developed between the propositional language of this logic and the first order language of K-algebras, analogously to the well known correspondence theory between classical normal modal logic and the first-order language of Kripke frames. In this paper, we develop such a theory for the class of analytic inductive inequalities.

ABSTRACT. We present cut-free labelled sequent calculi for various systems of inquisitive modal logic, including inquisitive epistemic logic and inquisitive doxastic logic. Inquisitive modal logic extends the framework of standard modal logic with a question-forming operator and an inquisitive modal operator. Under an epistemic interpretation, this modal operator may be used to express not only the information available to an agent, but also the issues entertained by the agent. Each of our proof systems is shown to satisfy cut-admissibility, height-preserving admissibility of weakening and contraction, and height-preserving invertibility of all rules. The completeness of our calculi is established proof-theoretically.

ABSTRACT. Lambek Calculus is a non-commutative substructural logic for formalising linguistic constructions. However, its domain of applicability is limited to constructions with local dependencies. We propose here a simple extension that allows us to formalise a range of relativised constructions with long distance dependencies, notably medial extractions and parasitic gaps. In proof theoretic terms, our logic combines commutative and non-commutative behaviour, as well as linear and non-linear resource management. This is achieved with a single restricted modality. But unlike other extensions of Lambek Calculus with modalities, our logic remains decidable, and the complexity of proof search (i.e., sentence parsing) is the same as for the basic Lambek calculus. Furthermore, we provide not only a sequent calculus, and a cut elimination theorem, but also proof nets.

ABSTRACT. Lawvere hyperdoctrines give categorical semantics for intuitionistic predicate logic but are flexible enough to be applied to other logics and extended to higher-order systems. We return to Ghilardi’s hyperdoctrine semantics for first-order modal logic and extend it in two directions—to weaker, non-normal modal logics and to higher-order modal logics. This includes soundness and completeness results, as well as a hyperdoctrinal version of the Gödel-McKinsey-Tarski translation from (normal) modal hyperdoctrines to intuitionistic hyperdoctrines. By focusing on non-normal modal logics, this work is intended to complement the other categorical semantics that have been developed for quantified modal logic, and may also be regarded as first steps to extend coalgebraic modal logic to first-order and higher-order settings via hyperdoctrines.

ABSTRACT. We introduce the f-cube which extends the original pure type system (PTS) cube, the λ-cube, with finite-set declarations (FSDs) like y ∈ {C, D} :B. Such a declaration is like the normal declaration y : B (which the f-cube also has), but adds the requirement that y can only become C or D. FSDs can express “definitions” and also singleton (or finite set) types/kinds, but are not the same as either. We prove for the f-cube the usual correctness properties such as subject reduction and strong normalization (SN) of type-correct terms. A result of Giannini, Honsell, and Ronchi is that the λ-cube with all type formation rules types the same pure untyped λ-terms as Fω, and Urzyczyn demonstrated a pure untyped λ- term U that is SN but is not typable in Fω, and therefore is also not typable in the λ-cube. We illustrate how to type U in the f-cube using an encoding of intersection types based on FSDs. Although the λ-cube with all type formation rules types the same pure untyped λ-terms as Fω, and thus fails to type many SN pure untyped λ-terms, we prove that the f-cube types all SN pure untyped λ-terms. We do this by translating into the f-cube all derivations of a system of intersection types. Notably, our translation works without needing in the target system (the f-cube) anything like the usual ∩-introduction rule that proves a pure untyped λ-term M has an intersection type Φ1 ∩ · · · ∩ Φk using k independent subderivations. Our approach might be useful for language implementers who want the power of intersection types without the pain of the ∩-introduction rule.