Algorithmic correspondence and canonicity for distributive modal logic

We define the algorithm ALBA for the language of the same distributive modal logic (DML) for which a Sahlqvist theorem was proved by Gehrke, Nagahashi, and Venema. Successful executions of ALBA compute the local first-order correspondents of input DML inequalities, and also guarantee their canonicity. The class of inequalities on which ALBA is successful is strictly larger than the newly introduced class of inductive inequalities, which in its turn properly extends the Sahlqvist inequalities of Gehrke et al. Evidence is given to the effect that, as their name suggests, inductive inequalities are the distributive counterparts of the inductive formulas of Goranko and Vakarelov in the classical setting.     

A Cayley theorem for distributive lattices

A Cayley-like representation theorem for distributive lattices is proved. Support of the research of the first author by the Czech Government Research Project MSM 6198959214 is gratefully acknowledged.     

A characterization theorem for geometric logic

We establish a criterion for deciding whether a class of structures is the class of models of a geometric theory inside Grothendieck toposes; then we specialize this result to obtain a characterization of the infinitary first-order theories which are geometric in terms of their models in Grothendieck toposes, solving a problem posed by Ieke Moerdijk in 1989.     

Two-dimensional modal logic

Prepositional logics with many modalites, characterized by two-dimensional Kripke models, are investigated. The general problem can be formulated as follows: from two modal logics describing certain classes of Kripke modal lattices construct a logic describing all products of Kripke lattices from these classes. For a large number of cases such a logic is obtained by joining to the original logics an axiom of the form _{ijp jip} and _{ijp jjp}. A special case of this problem, leading to the logic of a torus S5×S5 was solved by Segerberg [1].Translated from Matematieheskie Zametki, Vol. 23, No. 5, pp. 759–772, May, 1978.     

Generalization of fischer's theorem for distributive quasigroups

We generalize Fischer's well-known theorem which asserts that the right associated group of a finite distributive quasigroup is solvable. We prove that the associated group of a finitely generated distributive quasigroup is solvable and that the associated group of any distributive quasigroup is locally solvable.Translated from Matematicheskie Zametki, Vol. 23, No. 4, pp. 521–526, April, 1978.     

Deep sequent systems for modal logic

We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference but otherwise stay very close to Gentzen’s sequent calculus, in particular they enjoy a subformula property in the literal sense. No semantic notions are used inside the proof systems, in particular there is no use of labels. All their rules are invertible and the rules cut, weakening and contraction are admissible. All systems admit a straightforward terminating proof search procedure as well as a syntactic cut elimination procedure.      

An analog of Beth's theorem in normal extensions of the modal logic K4

Novosibirsk. Translated fromSibirskiî Matematicheskiî zhurnal, Vol. 33, No. 6, pp. 118–130, November–December, 1992.     

A double arity hierarchy theorem for transitive closure logic

In this paper we prove that thek-ary fragment of transitive closure logic is not contained in the extension of the (k–1)-ary fragment of partial fixed point logic by all (2k–1)-ary generalized quantifiers. As a consequence, the arity hierarchies of all the familiar forms of fixed point logic are strict simultaneously with respect to the arity of the induction predicates and the arity of generalized quantifiers.Although it is known that our theorem cannot be extended to the sublogic deterministic transitive closure logic, we show that an extension is possible when we close this logic under congruence.Supported by a grant from the University of Helsinki. This research was initiated while he was a Junior Researcher at the Academy of FinlandThis article was processed by the author using the LATEX style filepljourlm from Springer-Verlag.     

A modal logic framework for reasoning about comparative distances and topology

We propose and investigate a uniform modal logic framework for reasoning about topology and relative distance in metric and more general distance spaces, thus enabling the comparison and combination of logics from distinct research traditions such as Tarski’s S4 for topological closure and interior, conditional logics, and logics of comparative similarity. This framework is obtained by decomposing the underlying modal-like operators into first-order quantifier patterns. We then show that quite a powerful and natural fragment of the resulting first-order logic can be captured by one binary operator comparing distances between sets and one unary operator distinguishing between realised and limit distances (i.e., between minimum and infimum). Due to its greater expressive power, this logic turns out to behave quite differently from both S4 and conditional logics. We provide finite (Hilbert-style) axiomatisations and ExpTime-completeness proofs for the logics of various classes of distance spaces, in particular metric spaces. But we also show that the logic of the real line (and various other important metric spaces) is not recursively enumerable. This result is proved by an encoding of Diophantine equations.     

Provability interpretations of modal logic

We consider interpretations of modal logic in Peano arithmetic (P) determined by an assignment of a sentencev ^* ofP to each propositional variablev. We put (⊥)*=“0 = 1”, (χ → ψ)* = “χ* → ψ*” and let (□ψ)* be a formalization of “ψ)* is a theorem ofP”. We say that a modal formula, χ, isvalid if ψ* is a theorem ofP in each such interpretation. We provide an axiomitization of the class of valid formulae and prove that this class is recursive.     

A modal provability logic of explicit and implicit proofs

We establish the bi-modal forgetful projection of the Logic of Proofs and Formal Provability GLA. That is to say, we present a normal bi-modal provability logic with modalities □ and whose theorems are precisely those formulas for which the implicit provability assertions represented by the modality can be realized by explicit proof terms.