Wormshop 2017

Program

• Ana Borges
  
  A Calculus for Worms (Slides)

  In 2012, Dashkov described a calculus used to reason about a strictly positive fragment of the language of GLP. The sequent-style presentation of this calculus proposed by Beklemishev is called the Reflection Calculus (RC). It is well-known that every closed formula of RC can be equivalently written as a worm. One wonders whether it would be possible to work only with worms, maintaining the same proof power available in RC. The answer is yes. We present a calculus for worms and show that it proves exactly the same conjunction-free closed statements as the Reflection Calculus. We are also currently extending the results to creatures more exotic than worms. Joint work with Joost Joosten.

• Lorenzo Carlucci
  
  On the strength of Hindman's Theorem for bounded sums or unions (Slides)

  We report on recent results on the strength of restrictions of Hindman's Theorem to finite sums or unions, and variants theoreof. On the one hand we show that some weak restrictions already attain the known ACA_0 lower bound for the full theorem. On the other hand we show that some other weak restrictions also admit an ACA_0 upper bound, which is much lower than the only upper bound known on the full theorem, i.e. ACA_0^+. We also discuss connections with the Increasing Polarized Ramsey's Theorem and highlight the role of a sparsity condition on the solution set, which we call apartness. Part of this work is join with Kolodziejczyk, Lepore and Zdanowski.

• David Fernández Duque
  
  Caristi's fixed point theorem, non-monotone inductive definitions, and relativized leftmost paths (Slides)

  This is joint work with Paul Shafer, Henry Towsner and Keita Yokoyama.

  A Caristi system is a triple (X,f,V), where X is a complete metric space, V is a lower semi-continuous function from X to the positive reals, and f: X->X is an arbitrary function such that d(x,f(x)) <= V(x) - V(f(x)) always holds.
  Caristi's fixed point theorem states that any Caristi system has a fixed point. This has been proven in the literature using the Ekeland variational principle, and using Caristi sequences, which are transfinite iterations of f.
  We analyze Caristi's theorem and its known proofs in the context of reverse mathematics, where metric spaces are assumed separable and coded in the standard way. Among the results obtained, we have that, over RCA_0:
  + WKL_0 is equivalent to Caristi's theorem restricted to compact spaces with continuous V.
  + ACA_0 is equivalent to Caristi's theorem restricted to compact spaces with lower semi-continuous V.
  + Towsner's relativized leftmost path principle is equivalent to Caristi's theorem for Baire or Borel f.
  + The arithmetical inflationary fixed point scheme is equivalent to the statement that if f is arithmetically defined, any point of X can be included in a Caristi sequence containing a fixed point of f.
  These theories are all defined over the language of second-order arithmetic and we mention them in strictly increasing order of strength.

• Melvin Fitting
  
  How widespread are justification logics? (Slides)

  Justification logics have become fairly well-known. While they began with one instance, LP, having an important application to intuitionistic semantics, it has been found that man modal logics have justification counterparts. The extent of this is not yet understood. IRealization theorems are at the heart - justification counterpart should record how information is used in a modal validity for some modal logic. I will discuss recent progress in pushing the edges of the justification family further out, and what the current understanding is.

• Giorgi Japaridze
  
  Strong alternatives to weak arithmetics (Slides)

  I shall briefly survey arithmetical theories based on the game-semantically conceived Computability Logic. Such theories, dubbed “clarithmetics”, allow us to naturally and systematically capture various computational complexity classes, and do this in a stronger sense than weak arithmetics (e.g. bounded arithmetics) do. Specifically, due to being extensions rather than fragments of PA, clarithmetics achieve not only extensional but also intensional completeness with respect to their target complexity classes. The underlying concept of computability in clarithmetics is also more general than the traditional one, in that it is about interactive problems rather than merely about functions. In this world of interactive computability some unusual phenomena occur. E.g., space complexity is not necessarily upper-bounded by time complexity; not all computable problems have computable time complexities; interactive P has been separated from interactive PSPACE; and more.

• Dick de Jongh
  
  Do we really need Ex Falso? A first reconnaissance (Slides)

  Intuitionistic mathematics has been critized for the use of the Ex Falso principle, directly, or indirectly by disapproval of any use of negation at all. Do we really need it? Not in Heyting Arithmetic, if we agree with interpreting 1=0 as the falsum. We take some first steps looking around in other systems aided by some work by student Noor Heerkens.

• Joost J. Joosten
  
  Turing jumps again (Slides)

  We present an interpretation of transfinite polymodal provability logic in second order arithmetic that runs - contrary to the omega-rule interpretation - in phase with the degrees of the Turing jumps.

• Stepan Kuznetsov
  
  Iteration in residuated structures (Slides)

  We consider residuated semigroups, i.e., partially ordered semigroups with division operations, enriched with the positive iteration operation (an analog of Kleene star, but with the non-emptiness condition). There are two ways for defining iteration: by induction and by *-continuity; a standard example for the second approach is the powerset of the free semigroup a.k.a. the algebra of formal languages (without the empty word). We show that the atomic inequational theories for these two approaches differ. Note that for the non-residuated case the situation is different: as shown by Kozen, equational theories of Kleene algebras and the subclass of *-continuous Kleene algebras coincide. The proof is non-constructive and is based on complexity considerations: we show that the calculus for the *-continuous case, which is the Lambek calculus extended with infinitary rules for the iteration, has a Π⁰₁-complete derivability problem (we show it using methods by Buszkowski and Palka), and for the inductive system we have a circular proof system, which is definitely recursively enumerable. We also consider the Lambek calculus extended both with iteration and the (sub)exponential modality allowing the contraction rule (in the non-local form) and show that the complexity there is at least Π¹₁. Finally, we raise some open questions for future research, both technical (probably easy to solve, like translating the results from semigroups with positive iteration to monoids with Kleene iteration etc.) and significant (most importantly, completeness w.r.t. models on formal languages).

• Evgeny Kolmakov
  
  Axiomatizing provable 1-provability (Slides)

  We consider the following question for a pair of theories T and S: for which sentences their 1-provability in S is provable in T? The set of all such sentences forms a theory extending S. We give an axiomatization of this theory for the fragments of PA in terms of iterated local reflection schema over S.

• Mateusz Łełyk
  
  Prolongable Satisfaction Classes and Iterations of Uniform Reflection over PA (Slides)

  We study nonstandard models of iterations of uniform reflection over PA that contain a partial inductive satisfaction class. Our original motivation was to prove an analogue of the Enayat and Visser theorem that each partial inductive satisfaction class can be prolonged in an end-extension to a full satisfaction class (proved independently and unpublished) in the case of the ∆₀ inductive satisfaction class.
  To achieve our goal we introduced the notion of a prolongable satisfaction class: in words a class S on M is prolongable if there exists an elementary end extension N of M and a partial inductive satisfaction class S' on N which "covers" M and prolongs S. S is n-prolongable if this can be repeated n-times starting from S.
  It turned out that the existence of an n-prolongable partial inductive satisfaction class characterizes the models of n-iterated uniform reflection over PA (UR^n (PA)):

  Theorem 1. For a nonstandard model M |= PA having a partial inductive satisfaction class S the following are equivalent
  1. M |= URn (PA)
  2. S can be restricted to an n-prolongable satisfaction class.

  As a limit we obtain our desired theorem:

  Theorem 2. For a nonstandard model M |= PA having a partial inductive satisfaction class S the following are equivalent
  1. M |= UR^ω (PA)
  2. There exist a restriction S' of S, an elementary end extension N of M and a full ∆₀ inductive satisfaction class S'' on N such that S' ⊆ S''.

  Our methods consist in internalizing the standard existence arguments for partial inductive satisfaction classes. Moreover, Theorem 2, provides a new proof of conservativity of the theory CT₀ over UR^ω (PA) (the first was presented in [1]).

  References
  [1] Henryk Kotlarski. Bounded induction and satisfaction classes. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 32(31-34):531–544, 1986.

• Mauricio Martel
  
  Relation-changing modal logics: some model and proof theoretic aspects (Slides)

  We can fairly say that Logic (whichever you want to choose, be it propositional or first-order, classical or non-classical) is the mathematical tool used, par excellence, to describe a structure. Modal logics, for example, are particularly well suited to describe relational structures, specially if one is interested in computationally well behaved formalisms. But why can a logic only describe a structure? In this talk we introduce relation-changing modal logics, a family of modal logics that can change the accessibility relation of a model during the evaluation of a formula. We consider some model and proof theoretic aspects of relation-changing modal logics. We start by illustrating some inexpressible properties such as the tree and finite model properties, and we show that these logics can be seen as fragments of hybrid logics by providing satisfiability-preserving translations. Then, we present sound and complete tableau methods using hybrid logic tools, and we conclude with some open questions aiming at integrating relation-changing modal logics within the current landscape of logics of model update.

• Sergey Melikhov
  
  Kolmogorov's interpretation and a formal semantics of the meta-logic of intuitionistic logic

  I would like to report on a formal semantics capturing Kolmogorov's informal interpretation of intuitionistic logic in terms of problem solving.
  Kolmogorov's interpretation consists of two parts: one deals with the logical connectives and, implicitly, quantifiers, and is more or less the same as the so-called BHK interpretation; and the other deals with principles and rules and hence, implicitly, with the meta-logical connectives and quantifiers. The logical part has been extensively covered and discussed in the literature - albeit mostly in the terminology of Brouwer and Heyting, which forces a once-and-for-all choice between intuitionistic and classical logics despite their coexistence and interaction in Kolmogorov's approach. (Concerning this interaction see https://arxiv.org/abs/1312.2575 and https://arxiv.org/abs/1504.03379.)
  By contrast, the meta-logical part has been neglected. This is not surprising, as it turns out to be incompatible with the usual model theory, based on Tarski's notion of semantic consequence; worse yet, it is an interpretation of something that does not exist in the usual formalism of first-order logic (but exists, for instance, in the meta-logical formalism of the {\tt Isabelle} prover). However, ignoring the meta-logical part has the effect of throwing the baby out with the bathwater: as observed by Troelstra and van Dalen, "the BHK-interpretation in itself has no `explanatory power' ", since "on a very `classical' interpretation of [the informal notions of] construction and mapping," its six clauses "justify the principles of two-valued (classical) logic."
  To address these issues, we develop a formal semantics of Isabelle's meta-logic, or rather of its simplified version which suffices for first-order logics without equality. In usual model theory, regarded as a particular semantics of the meta-logic, the meta-logical connectives and quantifiers are interpreted classically (and moreover in the two-valued way) --- even though they are constructive. By interpreting them constructively, we get a generalized model theory, which covers, in particular, some realizability-type interpretations of intuitionistic logic.
  On the other hand, Kolmogorov's interpretation of inference rules (which is a substantial part of his interpretation of intuitionistic logic, and seems to be uniquely possible in his approach) is based on a notion of semantic consequence that is alternative to Tarski's standard notion, and is incompatible even with the generalized model theory. Thus we develop an alternative model theory, which is nothing new for formulas and principles, but an entirely different interpretation of rules (and of more complex meta-logical constructs). By using an extension of the meta-logic, we further get a generalized alternative model theory, which suffices to formalize Kolmogorov's interpretation of rules. See https://arxiv.org/abs/1504.03380.
  As a work in progress, we also develop a slightly different, "categorifed" semantics of the meta-logic, which in particular yields an interpretation of the meta-logic of (first-order) intuitionistic logic that has some intrinsic similarity with Voevodsky's interpretation of Martin-Löf's type theory with universes.

• Sergey Odintsov
  
  FDE-Modalities and weak definability (joint work with H. Wansing) (Slides)

  The goal of this talk is to compare various modal logics based on Belnap and Dunn's paraconsistent four-valued logic FDE. One of such logics is the modal logic BK defined by S. Odintsov and H. Wansing in 2010. Its extension BS4 (a natural counterpart of S4) relates to the paraconsistent Nelson's logic N4^⊥ in the same way as S4 relates to intuitionistic logic. Other versons of FDE-based modal logics are the paraconsistent modal logic KN4 by L. Goble whose non-modal base coincides with R. Brady's BD4 and the modal bilattice logic MBL introduced and investigated by A. Jung, U. Rivieccio, and R. Jansana. MBL is a generalization of BK that in its Kripke semantics makes use of a four-valued accessibility relation. On the way from BK to MBL, the Fischer Servi–style modal logic BK^FS is defined as the set of all modal formulas valid under a modified standard translation into first-order FDE. To compare the expressive power of these logics having the strong negation ∼ in the language we must weaken the notion of definitional equivalence in a suitable way. It is proved, e.g., that BK^FS is weakly definitionally equivalent to BK × BK and that MBL is faithfully embedded into BK × BK via a weakly structural translation.

• Fedor Pakhomov
  
  Solovay’s completeness without fixed points (Slides)

  We present a new proof of Solovay's theorem on arithmetical completeness of Gödel-Löb provability logic GL. Originally, completeness of GL with respect to interpretation of □ as provability in PA was proved by R. Solovay in 1976. The key part of Solovay's proof was his construction of an arithmetical evaluation for a given modal formula that made the formula unprovable PA if it were unprovable in GL. The arithmetical sentences for the evaluations were constructed using certain arithmetical fixed points. The method developed by Solovay have been used for establishing similar semantics for many other logics. In our proof we develop new more explicit construction of required evaluations that doesn't use any fixed points in their definitions. To our knowledge, it is the first alternative proof of the theorem that is essentially different from Solovay's proof in this key part. Also we use a similar technique to give an example of a natural Orey sentence for PA.

• Saeed Salehi
  
  Diagonal-free proofs of the Diagonal Lemma (Slides)

  The Diagonal Lemma (of Gödel and Carnap) is one of the fundamental results in Mathematical Logic. However, its proof (as presented in textbooks) is very un_intuitive, and a kind of "pulling a rabbit out of a hat". As a matter of fact, several theorems that are proved by using this lemma now have diagonal-free proofs. One example is Gödel's Incompleteness theorem for which several diagonal-free proofs are given by Kleene, Chaiting and Boolos; another example is Tarski's Undefinability theorem for which Robinson and Kotlarski gave diagonal-free proofs.
  In this talk we will see that a weak form of the Diagonal Lemma is equivalent with Tarski's theorem, and we will explore some different proofs for these theorems. Even though there will be no new theorem in this talk, several interesting proofs for old theorems will be presented.

• Kentaro Sato
  
  Negative Church's thesis and Russian constructivism (Slides)

  A variety of constructive mathematics, known as Russian Recursive Constructive Mathematics (RRCM), has been considered to be characterized by two axioms: the semi-classical principle called Markov's principle (MP) and Church's Thesis (CT) or its extended variant (ECT). The latter basically asserts that any function has a recursive index, and is known to be inconsistent with Brouwer's principle, namely the continuity of all functions on Baire space. I modify Church's Thesis with negative or classical existence (NCT), and show, by a realizability model, that it is consistent with Brouwer's principle as well as with many important consequences of the original CT or ECT. Intuitively, CT requires that if a function is given then its code is also given, whereas NCT does not require it but only that any function is recursive (without index being given). I would like to know the opinions especially from today's Russian logicians about this new principle with respect to RRCM, a Russian tradition from Markov.

• Yury Savateev
  
  Non-Well-Founded Proofs for Modal Grzegorczyk Logic (Slides)

  We present a sequent calculus for the modal Grzegorczyk logic Grz allowing non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs.

• Denis Saveliev
  
  Systems of propositions referring to each other: a model-theoretic view (Slides)

  We investigate arbitrary sets of propositions such that some of them state that some of them (possibly, themselves) are wrong, and criterions of paradoxicality or non-paradoxicality of such systems. For this, we propose a finitely axiomatized first-order theory with one unary and one binary predicates, T and U. An heuristic meaning of the theory is as follows: variables mean propositions, Tx means that x is true, Uxy means that x states that y is wrong, and the axioms express natural relationships of propositions and their truth values. A model (X,U) is called non-paradoxical iff it can be expanded to some model (X,T,U) of this theory, and paradoxical otherwise. E.g. a model corresponding to the Liar paradox consists of one reflexive point, a model for the Yablo paradox is isomorphic to natural numbers with their usual ordering, and both these models are paradoxical.

  We show that the theory belongs to the class Π⁰₂ but not Σ⁰₂ and is undecidable. We propose a natural classification of models of the theory based on a concept of collapsing models. Further, we show that the theory of non-paradoxical models, and hence, the theory of paradoxical models, belongs to the class Δ¹₁ but is not elementary. We consider also various special classes of models and establish their paradoxicality or non-paradoxicality. In particular, we show that models with reflexive relations, as well as models with transitive relations without maximal elements, are paradoxical; this general observation includes the instances of Liar and Yablo. On the other hand, models with well-founded relations, and more generally, models with relations that are winning in sense of a certain membership game are non-paradoxical. Finally, we propose a natural classification of non-paradoxical models based on the above-mentioned classification of models of our theory.

  This work was supported by grant 16-11-10252 of the Russian Science Foundation.

• Andre Scedrov
  
  Lambek calculus extended with subexponential and bracket modalities (Slides)

  The Lambek calculus (1958, 1961) is a well-known logical formalism for modelling natural language syntax. The calculus can also be considered as a version of non-commutative intuitionistic linear logic. The Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. The original calculus covered a substantial number of intricate natural language phenomena. In order to address more subtle linguistic issues, the Lambek calculus has been extended in various ways.

  For instance, an extension with so-called bracket modalities introduced by Morrill (1992) and Moortgat (1995) is capable of representing controlled non-associativity and is suitable for the modeling of islands. The syntax is more involved than the syntax of a standard sequent calculus. Derivable objects are sequents of the form Gamma --> A , where the antecedent Gamma is a structure called meta-formula and the succedent A is a formula. Meta-formulae are built from formulae (types) using two metasyntactic operators: comma and brackets.

  Morrill and Valentin (2015) introduce a further extension with so-called exponential modality, suitable for the modeling of medial and parasitic extraction. Their extension is based on a non-standard contraction rule for the exponential, which interacts with the bracket structure in an intricate way. The standard contraction rule for exponentials is not admissible in this calculus. In joint work with Max Kanovich and Stepan Kuznetsov we show that provability in this calculus is undecidable and we investigate restricted decidable fragments considered by Morrill and Valentin. We show that these fragments belong to NP.

• Paul Shafer
  
  The reverse mathematics of Ekeland's variational principle (Slides)

  (Joint with David Fernández-Duque, Henry Towsner, and Keita Yokoyama.)

  Let X be a complete metric space, and let V be a lower semi-continuous function from X to the non-negative reals. Ekeland's variational principle states that V has a 'critical point,' which is a point x* such that d(x*, y) > V(x*) - V(y) whenever y is not x*. This theorem has a variety of applications in analysis. For example, it implies that certain optimization problems have approximate solutions, and it implies a number of interesting fixed point theorems, including Caristi's fixed point theorem.

  We analyze the proof-theoretic strength of Ekeland's variational principle in the context of second-order arithmetic. We show that the full theorem is equivalent to Pi^1_1-CA_0. We also show that a few natural special cases, such as when V is assumed to be continuous and/or X is assumed to be compact, are equivalent to the much weaker systems ACA_0 and WKL_0.

• Valentin Shehtman
  
  Simplicial semantics of modal predicate logics (Slides)

  Simplicial semantics for modal and modal predicate logics was introduced by Dmitry Skvortsov in the early 1990s as a maximal Kripke-type semantics. Basic results on this semantics were proved by Skvortsov and Shehtman (1993). In this talk we present a new incompleteness result: there is a continuum of logics (some of which are very simply axiomatized) that are complete in simplicial semantics, but incomplete in Ghilardi's functor semantics. These logics are quantified versions of propositional modal logics above D4.1 (= K4+seriality+McKinsey formula).

• Stanislav Speranski
  
  On the computational aspects of Kripke's theory of truth (Slides)

  We shall discuss how to measure complexity of partial truth predicates arising in Kripke's theory of truth. Аpart from giving a survey of the topic, I shall present a method for proving complexity results in this direction, and show how to use it to obtain some interesting generalisations of known results. This method will be both relatively simple, involving only the basic machinery of constructive ordinals, and rather general.

• Albert Visser
  
  What is Gödel’s Second Incompleteness Theorem? (for joint session with Steklov Institute Mathematical Seminar) (Slides)

  Great mathematical theorems often have cloud-like identities, being more like a cloud of non-equivalent formulations than being one sharp result. Gödel’s incompleteness theorems are no exception to this rule. In the case of the Second Incompleteness Theorem, the situation is even more dramatic. There seems to be no precise mathematical formulation that covers our intuitive `coordinate-free' understanding of the theorem. How to formulate (a reasonable version of) the theorem? In my talk I address this question and provide some further information about the theorem. To be specific:
  1) I provide a reasonably general preliminary formulation of the Second Incompleteness Theorem.
  2) I discuss the matter of intensionality in metamathematics. An inportant example of intentionality is the
  fact that whether one has the second incompleteness theorem or not may depend on the choice of the representation of the axiom set.
  3) I consider two ways to address the problem of giving a coordinate-free formulation of the theorem.
  4) I provide some examples of less well-known applications of the theorem.

  The second incompleteness theorem revisited (Slides)

  We discuss a number of examples of theories-cum-axiomatizations where the Löb Conditions fail,but where we still have the Second Incompleteness Theorem. E.g., we provide a Σ⁰₁-axiomatization of Elementary Arithmetic for which the Löb Conditions fail.

• Mikhail Svyatlovsky
  
  On axiomatization and polytime decidability of the strictly positive fragment of K4.3 (Slides)

  We call a formula strictly positive, if it is built of propositional variables, conjunction and modal diamond operators. The strictly positive fragment (SP-fragment) of a logic L is the set of all provable in L implications A->B, where A and B are strictly positive formulas. E. V. Dashkov proved that Gödel-Löb provability logic GL and the logic K4 have the same SP-fragments.
  We study the SP-fragment of the logic K4.3 of all transitive linear frames. We give two different semantical characterizations of the fragmet. We will present a finite axiomatization of the SP-fragment of K4.3 and prove that it is polytime decidable.

• James Walsh
  
  On the inevitability of the consistency operator (Slides)

  ​It is a well-known empirical phenomenon that natural axiomatic theories are well-ordered by their consistency strength. ​ ​To investigate this phenomenon, we examine recursive monotonic functions on the​ ​ Lindenbaum algebra of EA. We prove that no such function sends every​ ​ consistent φ to a sentence with deductive strength strictly between​ ​ φ and (φ∧Con(φ)). We generalize this result to iterates of consistency into the effective transfinite. We then prove that for any recursive​ ​ monotonic function f, if there is an iterate of Con that bounds f everywhere, then f must be somewhere equal to an iterate of Con.

• Bartosz Wcisło
  
  Models of the compositional truth theory with bounded induction

  In [1], it has been shown that CT₀, a compositional truth theory with Δ₀-induction for the truth predicate, is not conservative over Peano Arithmetic. Subsequently, Mateusz Łełyk has shown that this theory proves the principle of first-order closure which states that the set of true sentences is closed under derivations in first-order logic.
  We show how the original proof combined with the refined result by Łełyk shows that in every model M of CT₀, the truth predicate may be presented as a sum of the predicates T_c which satisfy full induction scheme and compositional axioms for sentences of logical complexity at most c (i.e., with the syntactic tree of height at most c). The observation that the original argument of nonconservativeness of CT₀ yields this model-theoretic corollary is due to Ali Enayat.
  Using standard arguments, one can show that the theory CT₀ is arithmetically strictly weaker than CT, its counterpart with full induction. In particular, there exist models of PA which admit an expansion to a model of CT₀ but do not admit an expansion to a model of CT. In such models, there exists a family of compatible fully inductive truth predicates which are compositional for sentences of arbitrarily high logical complexity, but there is no truth predicate which is fully inductive and compositional for all sentences.
  The above result is closely related to a problem in the theory of models of Peano Arithmetic which asks whether the existence of inductive satisfaction classes compositional for Σ_c sentences for all c implies existence of a fully inductive satisfaction class.

  References
  [1] M. Łełyk and B. Wcisło, "Notes on bounded induction for the compositional truth predicate," The Review of Symbolic Logic, 10 pp. 455-480, 2017.

• Junhua Yu
  
  Instantial Neighborhood Logic - tableau, sequent calculus, and interpolation (Slides)

  Instantial Neighborhood Logic (INL) employs a two-sorted operator □. In INL, formula □(α_1,...,α_j;α_0) means, the current point has a neighborhood in which α_0 universally holds, and none of α_1,...,α_j universally fails. In my talk last year at Tbilisi State University, a tableau system for INL was presented. To continue, in this talk we convert that tableau system to a hyper-sequent calculus, and then to a (normal) sequent calculus G3inl. Based on a splitting version of G3inl, we will explain how Lyndon interpolation theorem of INL is constructively established.

• Michael Zakharyaschev
  
  Kripke Completeness of Strictly Positive Modal Logics over Meet-semilattices with Operators (Slides)

  Our concern is the completeness problem for strongly positive (SP) theories, that is, sets of implications between SP-terms built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, SP-theories have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi, and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations of a completeness theory that aims to answer the question whether the two semantics define the same consequence relations for a given SP-theory.

• Evgeny Zolin
  
  Axiomatic classes of models in modal logics (Slides)

  In the model theory for any formal language, the results called definability criteria play a fundamental role. These are theorems that give necessary and sufficient conditions for an arbitrary class of structures to be (finitely) axiomatizable (in the chosen language) or to be representable as the union of (finitely) axiomatizable classes (these four options are exhaustive in some sense). A prominent result of this kind is Keisler's theorem saying that a class of first-order structures is elementary if and only if it is closed under elementary equivalence and ultraproducts. In this talk we give a survey of known and new results of this kind for some modal languages and classes of (pointed) Kripke models (not frames).