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 sequentstyle presentation of this calculus proposed by Beklemishev is called the Reflection Calculus (RC). It is wellknown 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 conjunctionfree 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, nonmonotone 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 semicontinuous 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 semicontinuous 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 secondorder arithmetic and we mention them in strictly increasing order of strength.  Melvin Fitting
How widespread are justification logics? (Slides)
Justification logics have become fairly wellknown. 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 gamesemantically 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 upperbounded 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 omegarule 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 nonemptiness 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 nonresiduated 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 nonconstructive 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 nonlocal 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 1provability (Slides)
We consider the following question for a pair of theories T and S: for which sentences their 1provability 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 endextension 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 nprolongable if this can be repeated ntimes starting from S.
It turned out that the existence of an nprolongable partial inductive satisfaction class characterizes the models of niterated 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 nprolongable 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(3134):531–544, 1986.  Mauricio Martel
Relationchanging modal logics: some model and proof theoretic aspects (Slides)
We can fairly say that Logic (whichever you want to choose, be it propositional or firstorder, classical or nonclassical) 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 relationchanging 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 relationchanging 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 satisfiabilitypreserving translations. Then, we present sound and complete tableau methods using hybrid logic tools, and we conclude with some open questions aiming at integrating relationchanging modal logics within the current landscape of logics of model update.
 Sergey Melikhov
Kolmogorov's interpretation and a formal semantics of the metalogic 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 socalled BHK interpretation; and the other deals with principles and rules and hence, implicitly, with the metalogical 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 onceandforall 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 metalogical 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 firstorder logic (but exists, for instance, in the metalogical formalism of the {\tt Isabelle} prover). However, ignoring the metalogical part has the effect of throwing the baby out with the bathwater: as observed by Troelstra and van Dalen, "the BHKinterpretation 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 twovalued (classical) logic."
To address these issues, we develop a formal semantics of Isabelle's metalogic, or rather of its simplified version which suffices for firstorder logics without equality. In usual model theory, regarded as a particular semantics of the metalogic, the metalogical connectives and quantifiers are interpreted classically (and moreover in the twovalued way)  even though they are constructive. By interpreting them constructively, we get a generalized model theory, which covers, in particular, some realizabilitytype 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 metalogical constructs). By using an extension of the metalogic, 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 metalogic, which in particular yields an interpretation of the metalogic of (firstorder) intuitionistic logic that has some intrinsic similarity with Voevodsky's interpretation of MartinLöf's type theory with universes.  Sergey Odintsov
FDEModalities 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 fourvalued 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 FDEbased modal logics are the paraconsistent modal logic KN4 by L. Goble whose nonmodal 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 fourvalued 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 firstorder 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ödelLö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
Diagonalfree 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 diagonalfree proofs. One example is Gödel's Incompleteness theorem for which several diagonalfree proofs are given by Kleene, Chaiting and Boolos; another example is Tarski's Undefinability theorem for which Robinson and Kotlarski gave diagonalfree 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 semiclassical 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
NonWellFounded Proofs for Modal Grzegorczyk Logic (Slides)
We present a sequent calculus for the modal Grzegorczyk logic Grz allowing nonwellfounded proofs and obtain the cutelimination theorem for it by constructing a continuous cutelimination mapping acting on these proofs.
 Denis Saveliev
Systems of propositions referring to each other: a modeltheoretic 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 nonparadoxicality of such systems. For this, we propose a finitely axiomatized firstorder 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 nonparadoxical 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 nonparadoxical 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 nonparadoxicality. 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 wellfounded relations, and more generally, models with relations that are winning in sense of a certain membership game are nonparadoxical. Finally, we propose a natural classification of nonparadoxical models based on the abovementioned classification of models of our theory.
This work was supported by grant 161110252 of the Russian Science Foundation.

Andre Scedrov
Lambek calculus extended with subexponential and bracket modalities (Slides)
The Lambek calculus (1958, 1961) is a wellknown logical formalism for modelling natural language syntax. The calculus can also be considered as a version of noncommutative 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 socalled bracket modalities introduced by Morrill (1992) and Moortgat (1995) is capable of representing controlled nonassociativity 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 metaformula and the succedent A is a formula. Metaformulae are built from formulae (types) using two metasyntactic operators: comma and brackets.
Morrill and Valentin (2015) introduce a further extension with socalled exponential modality, suitable for the modeling of medial and parasitic extraction. Their extension is based on a nonstandard 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ándezDuque, Henry Towsner, and Keita Yokoyama.)
Let X be a complete metric space, and let V be a lower semicontinuous function from X to the nonnegative 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 prooftheoretic strength of Ekeland's variational principle in the context of secondorder arithmetic. We show that the full theorem is equivalent to Pi^1_1CA_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 Kripketype 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 cloudlike identities, being more like a cloud of nonequivalent 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 `coordinatefree' 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 coordinatefree formulation of the theorem.
4) I provide some examples of less wellknown applications of the theorem.The second incompleteness theorem revisited (Slides)
We discuss a number of examples of theoriescumaxiomatizations 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 (SPfragment) 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ödelLöb provability logic GL and the logic K4 have the same SPfragments.
We study the SPfragment 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 SPfragment of K4.3 and prove that it is polytime decidable.  James Walsh
On the inevitability of the consistency operator (Slides)
It is a wellknown empirical phenomenon that natural axiomatic theories are wellordered 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 firstorder closure which states that the set of true sentences is closed under derivations in firstorder 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 modeltheoretic 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. 455480, 2017.  Junhua Yu
Instantial Neighborhood Logic  tableau, sequent calculus, and interpolation (Slides)
Instantial Neighborhood Logic (INL) employs a twosorted 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 hypersequent 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 Meetsemilattices with Operators (Slides)
Our concern is the completeness problem for strongly positive (SP) theories, that is, sets of implications between SPterms built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, SPtheories have two natural semantics: meetsemilattices with monotone operators providing Birkhoffstyle calculi, and firstorder 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 SPtheory.
 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 firstorder 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).