Logic, Language, Information, and Computation

Table of Contents

1. Frontmatter

2. Strict-Tolerant Conditional Logics

   Lin Chen, Xuefeng Wen

   Abstract

   We construct a conditional logic using selection models in a three-valued setting. When the selection function selects an empty set, the corresponding conditional is neither true nor false. The semantic consequence is defined as in Strict-Tolerant logic. The resulting logic validates Conditional Excluded Middle without assuming that a selection function always chooses a single world, reconciling Stalnaker and Lewis. We give a labelled sequent calculus for the logic and consider three extensions of it. It turns out two extensions are strongly connexive, hyperconnexive, superconnexive, and almost totally connexive.

3. A Linear Proof Language for Second-Order Intuitionistic Linear Logic

   Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe

   Abstract

   We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level.

4. A Logic of Isolation

   Can Başkent, David Gilbert, Giorgio Venturi

   Abstract

   In the vein of recent work that provides non-normal modal interpretations of various topological operators, this paper proposes a modal logic for a spatial isolation operator. Focussing initially on neighborhood systems, we prove several characterization results, demonstrating the adequacy of the interpretation and highlighting certain semantic insensitivities that result from the relative expressive weakness of the isolation operator. We then transition to the topological setting, proving a result for discrete spaces.

5. A Simple Loopcheck for Intuitionistic K

   Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, Lutz Straßburger

   Abstract

   In this paper, we present an algorithm for establishing decidability and finite model property of intuitionistic modal logic IK. These two results have been previously established independently by proof theoretic and model theoretic techniques respectively. Our algorithm, by contrast, enables us to establish both properties at the same time and simplifies previous approaches. It implements root-first proof search in a labelled sequent calculus that employs two binary relations: one corresponding to the modal accessibility relation and the other to the preorder relation of intuitionistic models. As a result, all the rules become invertible, hence semantic completeness could be established directly by extracting a (possibly infinite) countermodel from a failed proof attempt. To obtain the finite model property, we rather introduce a simple loopcheck ensuring that root-first proof search always terminates. The resulting finite countermodel displays a layered structure akin to that of intuitionistic first-order models.

6. A Compositional Theory of Krivine’s Classical Realisability

   Daichi Hayashi, Graham E. Leigh

   Abstract

   This paper presents a formal theory of Krivine’s classical realisability interpretation for first-order Peano arithmetic (\(\textsf{PA}\)). To formulate the theory as an extension of \(\textsf{PA}\), we first modify Krivine’s original definition to the form of number realisability, similar to Kleene’s intuitionistic realisability for Heyting arithmetic. By axiomatising our realisability with additional predicate symbols, we obtain a first-order theory \(\textsf{CR}\) which can formally realise every theorem of \(\textsf{PA}\). Although \(\textsf{CR}\) itself is conservative over \(\textsf{PA}\), adding a type of reflection principle that roughly states that “realisability implies truth” results in \(\textsf{CR}\) being essentially equivalent to the Tarskian theory \(\textsf{CT}\) of typed compositional truth, which is known to be proof-theoretically stronger than \(\textsf{PA}\). We also prove that a weaker reflection principle which preserves the distinction between realisability and truth is sufficient for \(\textsf{CR}\) to achieve the same strength as \(\textsf{CT}\).

7. Intersection Types via Finite-Set Declarations

   Fairouz Kamareddine, Joe Wells

   Abstract

   The \(\lambda \)-cube is a famous pure type system (PTS) cube of eight powerful explicit type systems that include the simple, polymorphic and dependent type theories. The \(\lambda \)-cube only types Strongly Normalising (SN) terms but not all of them. It is well known that even the most powerful system of the \(\lambda \)-cube can only type the same pure untyped \(\lambda \)-terms that are typable by the higher-order polymorphic implicitly typed \(\lambda \)-calculus \(F_\omega \), and that there is an untyped \(\lambda \)-term \(\dot{U}\) that is SN but is not typable in \(F_\omega \) or the \(\lambda \)-cube. Hence, neither system can type all the SN terms it expresses. In this paper, we present the \(\textsf {f}\)-cube, an extension of the \(\lambda \)-cube with finite-set declarations (FSDs) like \(y \mathord {\overline{\in }}\{C_1,\cdots , C_n\} :B\) which means that y is of type B and can only be one of \(C_1, \cdots , C_n\). The novelty of our FSDs is that they allow to represent intersection types as \(\varPi \)-types. We show how to translate and type the term \(\dot{U}\) in the f-cube using an encoding of intersection types based on FSDs. Notably, our translation works without needing anything like the usual troublesome intersection-introduction rule that proves a pure untyped \(\lambda \)-term M has an intersection type \(\varPhi _1\cap \cdots \cap \varPhi _k\) using k independent subderivations. As such, our approach is useful for language implementers who want the power of intersection types without the pain of the intersection-introduction rule.

8. Syntactic Concept Lattice Models for Infinitary Action Logic

   Stepan L. Kuznetsov

   Abstract

   We introduce models for infinitary action logic, i.e., the infinitary extension of multiplicative-additive Lambek calculus with the Kleene star, on syntactic concept lattices. This semantics is a variant of language semantics, which is in a sense more natural from the linguistic point of view. Extending the argument of Wurm (2017), we prove completeness for the whole infinitary action logic, while standard language models enjoy completeness only for small fragments of this system. As a corollary, we obtain completeness of infinitary action logic w.r.t. action lattices which are complete in the lattice-theoretic sense.

9. Rules of Partial Orthomodularity

   Mena Leemhuis, Diedrich Wolter, Özgür L. Özçep

   Abstract

   The rule of orthomodularity is important, for example due to its foundational role in quantum logic. However, orthomodularity is a restriction that is not always suitable. For example, orthomodularity is not fulfilled by certain geometric structures such as the lattice of closed convex cones, which is different from the lattice considered in quantum logic, namely that of closed subspaces of a Hilbert space. Thus, the question arises whether the rule of orthomodularity can be relaxed such that the relaxed rule is still stronger than the ortholattice rule and such that each orthomodular lattice fulfills also the relaxed rule. Therefore, we present two rules of partial orthomodularity of different strength, (pOM) and (pOM\(_{ex}\)), which keep some of the advantages of the rule of orthomodularity but are relaxations of it. We show the validity and usefulness of these rules by proving a subalgebra theorem for (pOM), by showing that an algebraic representation theorem for orthomodularity can be relaxed as to be based on the rules of partial orthomodularity and by proving a connection to Johansson’s minimal rule.

10. Labelled Sequent Calculi for Inquisitive Modal Logics

    Valentin Müller

    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.

11. Correspondence Theory on Vector Spaces

    Alessandra Palmigiano, Mattia Panettiere, Ni Wayan Switrayni

    Abstract

    This paper extends correspondence theory to the framework of \(\mathbb {K}\)-algebras, i.e. vector spaces endowed with a bilinear operation, seen as ‘Kripke frames’. For every \(\mathbb {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 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 \(\mathbb {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.

12. An EXPTIME-Complete Entailment Problem in Separation Logic

    Nicolas Peltier

    Abstract

    Separation logic (SL) is extensively employed in verification to analyze programs that manipulate dynamically allocated memory. The entailment problem, when dealing with inductively defined predicates or data constraints, is undecidable for SL formulas. Our focus is on addressing a specific fragment of this issue, wherein the consequent is restricted to clauses of some particular form, devoid of inductively defined predicates. We present an algorithm designed to determine the validity of such entailments and demonstrate that the problem is decidable and ExpTime complete under some conditions on the data theory. This algorithm serves the purpose of verifying that the data structures outlined by a given SL formula (the antecedent) adhere to certain shape constraints expressed by the consequent.

13. (In)consistency Operators on Quasi-Nelson Algebras

    Umberto Rivieccio, Aldo Figallo-Orellano

    Abstract

    We propose a preliminary study of (in)consistency operators on quasi-Nelson algebras, a variety that generalizes both Nelson and Heyting algebras; our aim is to pave the way for introducing logics of formal inconsistency (LFIs) in a non-necessarily involutive setting. We show how several results that were obtained for LFIs 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 characterize 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.

14. Lambek Calculus with Banged Atoms for Parasitic Gaps

    Mehrnoosh Sadrzadeh, Lutz Straßburger

    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 the challenging case of 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.

15. Completeness of Finitely Weighted Kleene Algebra with Tests

    Igor Sedlár

    Abstract

    Building on Ésik and Kuich’s completeness result for finitely weighted Kleene algebra, we establish relational and language completeness results for finitely weighted Kleene algebra with tests. Similarly as Ésik and Kuich, we assume that the finite semiring of weights is commutative, partially ordered and zero-bounded, but we also assume that it is integral. We argue that finitely weighted Kleene algebra with tests is a natural framework for equational reasoning about weighted programs in cases where an upper bound on admissible weights is assumed.

16. Modal Hyperdoctrine: Higher-Order and Non-normal Extensions

    Florrie Verity, Yoshihiro Maruyama

    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 [3] and extend it in two directions—to weaker, non-normal modal logics and to higher-order modal logics. We also relate S4 modal hyperdoctrines to intuitionistic hyperdoctrines via a hyperdoctrinal version of the Gödel-McKinsey-Tarski translation. 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.

17. Validity in Contexts

    A Semantics for Indicatives and Epistemic Modals Xuefeng Wen

    Abstract

    Inspired by McGee’s semantics for conditionals, we define a language with contexts explicitly encoded in formulas to evaluate propositions under assumptions. We give a three-valued semantics for the language and define a ternary notion of validity, unifying two kinds of validity in the literature. By the new notion of validity, an inference is not just valid or invalid, but valid or invalid under a set of assumptions. Based on the three-valued semantics and ternary notion of validity, we give a unified solution to some typical puzzles concerning indicatives and epistemic modals.

18. Logical Expressibility of Syntactic NL for Complementarity and Maximization

    Tomoyuki Yamakami

    Abstract

    In a discussion on the computational complexity of “parameterized” NL (nondeterministic logarithmic-space complexity class), Syntactic NL or succinctly SNL was first introduced in 2017 as a “syntactically”-defined natural subclass of NL using a restricted form of second-order logic in close connection to the so-called linear space hypothesis. We further explore various properties of this complexity class SNL. In particular, we consider the expressibility of “complementary” problems of SNL problems. As a variant of \(\textrm{SNL}\), we also study an optimization version of SNL, called MAXSNL, and its natural subclass, called MAX\(\tau \)SNL.

19. Polyadic Quantifiers on Dependent Types

    Marek Zawadowski, Justyna Grudzińska

    Abstract

    An interaction between dependency relations and quantification underlies numerous phenomena in natural language. Dependencies are responsible for inverting scope, as illustrated by the example a day of every month. The part-whole relation, expressed by the preposition of in this example, introduces a dependency between wholes (months) and their respective parts (days). Quantifying over this dependency yields the inverse scope reading: for every month, there is a different day that belongs to it. Dependencies are also needed for tracking anaphoric reference to quantifier domains, as illustrated by the sentence Every farmer who owns a donkey beats it. By quantifying universally over the dependency between each of the farmers and the donkeys owned by them, we obtain the intended reading that every farmer beats every donkey he owns. In this paper, we show that polyadic quantifiers on dependent types are well-suited for modelling the interaction of dependency relations and quantification in these phenomena. Then we present, in a conceptual way, the mathematics behind the process of polyadic quantification over dependent types. The main new feature is the left strength on the cartesian monad over a basic fibration of a topos. It combines with what we call the right strength into an operation (pile’up) that turns tuples of quantifiers into polyadic ones.

20. Backmatter