arXiv subjects
Publications and source records attributed to Tadeusz Litak.
We introduce relational semantics for "flat Heyting-Lewis logic" HLC-flat. This logic arises as the extension of intuitionistic logic with a Lewis-style strict implication modality that, contrary to its "sharp" counterpart HLC-sharp, does not turn meets into joins in its first argument. We prove completeness and the finite model property for HLC-flat and for several extensions with additional axioms.
Heyting-Lewis Logic is the extension of intuitionistic propositional logic with a strict implication connective that satisfies the constructive counterparts of axioms for strict implication provable in classical modal logics. Variants of this logic are surprisingly widespread: they appear as Curry-Howard correspondents of (simple type theory extended with) Haskell-style arrows, in preservativity logic of Heyting arithmetic, in the proof theory of guarded (co)recursion, and in the generalization of intuitionistic epistemic logic. Heyting-Lewis Logic can be interpreted in intuitionistic Kripke frames extended with a binary relation to account for strict implication. We use this semantics to define descriptive frames (generalisations of Esakia spaces), and establish a categorical duality between the algebraic interpretation and the frame semantics. We then adapt a transformation by Wolter and Zakharyaschev to translate Heyting-Lewis Logic to classical modal logic with two unary operators. This allows us to classical results to obtain the finite model property and decidability for a large family of Heyting-Lewis logics.
In 1984, Wim Ruitenburg published a surprising result about periodic sequences in intuitionistic propositional calculus (IPC). The property established by Ruitenburg naturally generalizes local finiteness; recall that intuitionistic logic is not locally finite, even in a single variable. One of the two main goals of this note is to illustrate that most "natural" non-classical logics failing local finiteness also do not enjoy the periodic sequence property. IPC is quite unique in separating these properties. The other goal of this note is to present a Coq formalization of Ruitenburg's heavily syntactic proof. Apart from ensuring its correctness, the formalization allows extraction of a program providing a certified implementation of Ruitenburg's algorithm.
Propositional inquisitive logic is the limit of its $n$-bounded approximations. In the predicate setting, however, this does not hold anymore, as discovered by Ciardelli and Grilletti, who also found complete axiomatizations of $n$-bounded inquisitive logics $\mathsf{InqBQ}_{n}$, for every fixed $n$. We introduce cut-free labelled sequent calculi for these logics. We illustrate the intricacies of \textit{schematic validity} in such systems by showing that the well-known Casari formula is \textit{atomically} valid in (a weak sublogic of) predicate inquisitive logic $\mathsf{InqBQ}$, fails to be schematically valid in it, and yet is schematically valid under the finite boundedness assumption. The derivations in our calculi, however, are guaranteed to be schematically valid whenever a single specific rule is not used.
In this paper, we introduce a novel team semantics of LTL inspired by inquisitive logic. The main features of the resulting logic, we call InqLTL, are the intuitionistic interpretation of implication and the Boolean semantics of disjunction. We show that InqLTL with Boolean negation is highly undecidable and strictly less expressive than TeamLTL with Boolean negation. On the positive side, we identify a meaningful fragment of InqLTL with a decidable model-checking problem which can express relevant classes of hyperproperties. To the best of our knowledge, this fragment represents the first hyper logic with a decidable model-checking problem which allows unrestricted use of temporal modalities and universal second-order quantification over traces.
We study the principle phi implies box phi, known as `Strength' or `the Completeness Principle', over the constructive version of Löb's Logic. We consider this principle both for the modal language with the necessity operator and for the modal language with the Lewis arrow, where Löb's Logic is suitably adapted. Central insights of provability logic, like the de Jongh-Sambin Theorem and the de Jongh-Sambin-Bernardi Theorem, take a simple form in the presence of Strength. We present these simple versions. We discuss the semantics of two salient systems and prove uniform interpolation for both. In addition, we sketch arithmetical interpretations of our systems. Finally, we describe the various connections of our subject with Computer Science.
In this paper, we tell a story about incompleteness in modal logic. The story weaves together a paper of van Benthem, `Syntactic aspects of modal incompleteness theorems,' and a longstanding open question: whether every normal modal logic can be characterized by a class of completely additive modal algebras, or as we call them, V-BAOs. Using a first-order reformulation of the property of complete additivity, we prove that the modal logic that starred in van Benthem's paper resolves the open question in the negative. In addition, for the case of bimodal logic, we show that there is a naturally occurring logic that is incomplete with respect to V-BAOs, namely the provability logic GLB. We also show that even logics that are unsound with respect to such algebras do not have to be more complex than the classical propositional calculus. On the other hand, we observe that it is undecidable whether a syntactically defined logic is V-complete. After these results, we generalize the Blok Dichotomy to degrees of V-incompleteness. In the end, we return to van Benthem's theme of syntactic aspects of modal incompleteness.
Our paper is the first study of what one might call "reverse mathematics of explicit fixpoints". We study two methods of constructing such fixpoints for formulas whose principal connective is the intuitionistic Lewis arrow. Our main motivation comes from metatheory of constructive arithmetic, but the systems in question allows several natural semantics. The first of these methods, inspired by de Jongh and Visser, turns out to yield a well-understood modal system. The second one by de Jongh and Sambin, seemingly simpler, leads to a modal theory that proves harder to axiomatize in an elegant way. Apart from showing that both theories are incomparable, we axiomatize their join and investigate several subtheories, whose axioms are obtained as fixpoints of simple formulas. We also show that they are extension stable, that is, their validity in the corresponding preservativity logic of a given arithmetical theory transfer to its finite extensions.
We overview the logic of Bunched Implications (BI) and Separation Logic (SL) from a perspective inspired by Hiroakira Ono's algebraic approach to substructural logics. We propose generalized BI algebras (GBI-algebras) as a common framework for algebras arising via "declarative resource reading", intuitionistic generalizations of relation algebras and arrow logics and the distributive Lambek calculus with intuitionistic implication. Apart from existing models of BI (in particular, heap models and effect algebras), we also cover models arising from weakening relations, formal languages or more fine-grained treatment of labelled trees and semistructured data. After briefly discussing the lattice of subvarieties of GBI, we present a suitable duality for GBI along the lines of Esakia and Priestley and an algebraic proof of cut elimination in the setting of residuated frames of Galatos and Jipsen. We also show how the algebraic approach allows generic results on decidability, both positive and negative ones. In the final part of the paper, we gently introduce the substructural audience to some theory behind state-of-art tools, culminating with an algebraic and proof-theoretic presentation of (bi-)abduction.
This paper generalizes the 1977 paper of V.B. Shehtman, which constructed the first Kripke incomplete intermediate logic, by presenting a continuum of such logics. This version fixes an error in my simplified proof of incompleteness of Shehtman's original logic.
I investigate the superintuitionistic analogue of the modal logic of chequered subsets of $\mathbb{R}^\infty$ introduced by van Benthem et al. It is observed that this logic possesses the disjunction property, contains the Scott axiom, fails to contain the Kreisel-Putnam axiom and it is a sublogic of the Medvedev logic.
We propose a generalization of first-order logic originating in a neglected work by C.C. Chang: a natural and generic correspondence language for any types of structures which can be recast as Set-coalgebras. We discuss axiomatization and completeness results for several natural classes of such logics. Moreover, we show that an entirely general completeness result is not possible. We study the expressive power of our language, both in comparison with coalgebraic hybrid logics and with existing first-order proposals for special classes of Set-coalgebras (apart from relational structures, also neighbourhood frames and topological spaces). Basic model-theoretic constructions and results, in particular ultraproducts, obtain for the two classes that allow completeness---and in some cases beyond that. Finally, we discuss a basic sequent system, for which we establish a syntactic cut-elimination result.
C. I. Lewis invented modern modal logic as a theory of "strict implication". Over the classical propositional calculus one can as well work with the unary box connective. Intuitionistically, however, the strict implication has greater expressive power than the box and allows to make distinctions invisible in the ordinary syntax. In particular, the logic determined by the most popular semantics of intuitionistic K becomes a proper extension of the minimal normal logic of the binary connective. Even an extension of this minimal logic with the "strength" axiom, classically near-trivial, preserves the distinction between the binary and the unary setting. In fact, this distinction and the strong constructive strict implication itself has been also discovered by the functional programming community in their study of "arrows" as contrasted with "idioms". Our particular focus is on arithmetical interpretations of the intuitionistic strict implication in terms of preservativity in extensions of Heyting's Arithmetic.
I overview the work of the Tbilisi school on intuitionistic modal logics of well-founded/scattered structures and its connections with contemporary theoretical computer science. Fixed-point theorems and their consequences are of particular interest.
Motivated by the recent interest in models of guarded (co-)recursion, we study their equational properties. We formulate axioms for guarded fixpoint operators generalizing the axioms of iteration theories of Bloom and Ésik. Models of these axioms include both standard (e.g., cpo-based) models of iteration theories and models of guarded recursion such as complete metric spaces or the topos of trees studied by Birkedal et al. We show that the standard result on the satisfaction of all Conway axioms by a unique dagger operation generalizes to the guarded setting. We also introduce the notion of guarded trace operator on a category, and we prove that guarded trace and guarded fixpoint operators are in one-to-one correspondence. Our results are intended as first steps leading, hopefully, towards future description of classifying theories for guarded recursion.
Motivated by the recent interest in models of guarded (co-)recursion we study its equational properties. We formulate axioms for guarded fixpoint operators generalizing the axioms of iteration theories of Bloom and Esik. Models of these axioms include both standard (e.g., cpo-based) models of iteration theories and models of guarded recursion such as complete metric spaces or the topos of trees studied by Birkedal et al. We show that the standard result on the satisfaction of all Conway axioms by a unique dagger operation generalizes to the guarded setting. We also introduce the notion of guarded trace operator on a category, and we prove that guarded trace and guarded fixpoint operators are in one-to-one correspondence. Our results are intended as first steps leading to the description of classifying theories for guarded recursion and hence completeness results involving our axioms of guarded fixpoint operators in future work.