Talks

As follows from their name, tree-hypersequents (also known as nested sequents) were created to represent the tree structure of underlying Kripke models. While this approach works well on modal and intermediate logics complete w.r.t. many types of tree-like frames, it is not directly suited to encode quantitative restrictions on these frames, e.g., bounded depth and/or bounded number of children per node. In order to capture these restrictions, we add the injectivity condition to nested sequents requiring different sequent nodes to correspond to distinct worlds in the underlying Kripke model. The downside is the loss of the formula interpretation. On the plus side, we show how the injective nested sequents can be used to constructively prove the Craig interpolation property for all interpolable intermediate logics strictly between the intuitionistic and classical propositional logics that are complete with respect to tree-like models, i.e., Smetanich logic (also known as the logic of here and there), the greatest semiconstructive logic, logic BD_2 of bounded depth 2, and Gödel logic. For the last one, we obtain a stronger form of interpolation called Lyndon interpolation.

As recently formulated by Yoram Moses, actions are not based on facts but rather on our knowledge of facts. This Knowledge of Preconditions Principle (KoP) underscores the central role that knowledge plays in decision making. The propagation of information in asynchronous in asynchronous distributed systems, i.e., those where agents do not have access to a global synchronized clock, has been well studied. It can rely solely on chains of messages, which form what Leslie Lamport called a causal cone. Until recently, this causality analysis existed only for fault-free systems and systems with very restricted types of faults. In our talk, we generalize the concept of the causal cone to systems with arbitrary byzantine failures and extract necessary conditions for achievable states of knowledge in fault-tolerant distributed systems.

To prove the correctness of a given distributed algorithm, it is necessary to verify that each action is taken only when the global system state allows it. However, due to the incomplete local view of each agent, the Knowledge of Preconditions Principle (KoP), formulated by Yoram Moses, lifts preconditions to the epistemic level. KoP states that, for any condition that is specified as necessary for an agent to perform a certain action, this agent knowing that the condition is fulfilled is also necessary for performing this action. It is well known that causality in asynchronous distributed systems, i.e., those where agents do not have access to a global synchronized clock, is governed solely by messages the agents exchange: an agent cannot know what happened to another agent without a chain of messages delivering this information, leading to the concept of a causal cone, first introduced by Leslie Lamport.

In this talk, we discuss the impact of byzantine failures on causality in asynchronous systems. If any agent can arbitrarily violate its protocol, e.g., send incorrect information, possibly different information to different respondents, then a simple chain of messages is not sufficient anymore. We provide an elaborate modeling and analysis framework for multi-agent systems with byzantine faults and use it to describe the byzantine analog of Lamport's causal cone, the limitations on what can be known in principle, as well as the necessary conditions for achievable states of knowledge in fault-tolerant distributed systems.

The idea to analyze communication in distributed systems using epistemic logic has been around for more than 25 years and yielded such seminal results as the necessity of common knowledge as a precondition for coordinated action. The goal of this ongoing project is to incorporate Byzantine agents, i.e., agents prone to failure, into the epistemic framework. Some limited types of Byzantine behaviours, e.g., crash failures, have already been studied in this respect by Dwork and Moses. But handling knowledge in such limited circumstances is more straightforward. We consider fully Byzantine agents whose behavior is maximally unrestricted but whose knowledge remains local. The failures of such agents to follow their protocol can be assigned either to malicious intent or to malfunction. It is the latter case that is of most interest from the epistemic perspective. One of the natural questions is whether such an agent can determine its own correctness or its own faultiness based solely on its local view of the system. In order to analyze such agents, we develop a detailed layered view of each transition step in a distributed system and prove first lower bounds on the communication necessary for performing actions despite at most f agents potentially failing. We demonstrate the potential of our framework by providing a modular way of incorporating into it various popular communication contexts, including synchronous agents, synchronous communication, broadcast (both hardware and software), coordinated action, etc.

Justification logic is a refinement of modal logic that views the modality as an existential quantifier over justifications. Thus, both modal and justification logic can be viewed as sublanguages of the same first-order language with terms ranging over justifications. In the talk we explore how Herbrandization emerged as a stepping stone in proving the Realization Theorem, one of the central results in justification logic, providing its connection to modal logic.

This talk will summarize the quest for achieving constructive interpolation results by proof-theoretic means, which started 5 years ago in Bern. We will present the general view of sequent-like formalisms for classical and intermediate logics that makes them susceptible to interpolation proofs and present the results for hypersequents, nested sequents, and labelled sequents. We will also discuss a curious case of Gödel logic, the interpolation for which cannot be proved using the standard hypersequent or labelled sequent calculi but can be proved using linear nested sequents, recently developed by Björn Lellmann.

We introduce a new Gentzen-style framework of grafted hypersequents that combines the formalism of nested sequents with that of hypersequents. To illustrate the potential of the framework, we present novel calculi for the modal logics K5 and KD5, as well as for extensions of the modal logics K and KD with the axiom for shift reflexivity. The latter of these extensions is also known as SDL^+ in the context of deontic logic. All our calculi enjoy syntactic cut elimination and can be used in backwards proof search procedures of optimal complexity.

Modal public announcement logics study how public announcements affect changes in beliefs of the agents. What cannot be expressed in these logics, however, is the exact reasons for the updated beliefs. Justification Logic suggests a way of filling this gap by representing evidence and/or justifications for agents' beliefs in the object language. We present two alternative justification counterparts of Gerbrandy–Groeneveld's logic of public introspective announcements over the basic modal logic K. In particular, we show that erasing justifications for belief in either of the two suggested counterparts yields a valid modal statement about announcements. For the opposite direction, we establish a constructive procedure for restoring justifications within modalities, a process called realization, for one of the suggested counterparts provided the modalities occur outside of announcements. We discuss how recording more information about announcements in our system of justifications in the other suggested counterpart creates difficulties for applying the method of "realization by reduction" we have developed.

Craig interpolation is known to hold for many modal logics. The proof-theoretic way of demonstrating it is by using induction on a cut-free derivation in a suitable sequent calculus. But for several modal logics cut-free sequent systems are not known. It is natural then to consider generalizations of sequent calculi that capture more modal logics in a cut-free way, such as labelled sequents and/or nested sequents. While it is not clear how to perform induction interpolation proof for the former, nested sequents seem well suited for the task due to the absence of semantical elements in the calculus. Despite this, the only use of nested sequents to prove interpolation we are aware of is due to Marta Bílková. Her method deals only with uniform interpolation and only for the basic normal logic K. We present a general framework for proving interpolation by induction on a nested-sequent derivation. The method, a joint work with Melvin Fitting, is inspired by prefixed sequent calculi that he recently introduced as a formalism, intermediate between nested sequents and prefixed tableaus. We discuss how our method applies to normal modal logics axiomatized using axioms d, t, b, 4, and 5 in various combinations.

Justification counterparts for most modal logics in the so-called “modal cube” are known. However, until recently there was no uniform method of proving the Realization Theorem for all of them. We present such a method for all the normal modal logics formed from the axioms d, t, b, 4, and 5. The main tools used are cut-free nested sequent calculi a la Kai Brünnler and Melvin Fitting's realization merging technique.

Based on our realization method, we discuss the question of modularity of realizations: each modal axiom has a natural justification counterpart. However, one modal logic may have several axiomatizations, accordingly it is natural to suggest there to be several natural justification counterparts, one for each axiomatization. Our goal is to completely classify these various realizations by introducing a natural equivalence relation on them that extends that of Fitting. The naturality of the equivalence relation here means that justification logics are equivalent iff they have the same forgetful projection.

Public Announcement Logic PAL was created by Jan Plaza in 1989. It describes how agents' knowledge is updated after public announcements. In 1997, Gerbrandy and Groeneveld independently developed a similar logic that describes updates of agents' beliefs in settings where the announced facts need not be true.

Logics from the family of Artemov's Logic of Proofs have been successfully used to realize modal epistemic logics and analyze evidence behind knowledge/beliefs. Our goal is to expand this method of study to the logic of public announcement. We will present two candidate logics, JPAL and OPAL, describe their update semantics and formulate a partial realization theorem. We will also discuss the challenges on the way to the full realization.

In this talk, we discuss how the language of justification logic can be effectively used to describe belief revision that arises as a result of public announcements. The field of belief revision investigates how one's beliefs can be represented in a logical framework and how changes in beliefs upon receipt of new information can be described axiomatically. Dependent on the intended application, different logical formalisms can be employed to describe initial and modified beliefs. Beliefs about "real-world" facts — but not about the beliefs of other agents (e.g., database model) — can be represented as a belief set, i.e., a set of all facts that the agent believes, which must be closed under logical consequence. In this approach, the operation of belief change is performed on a meta-level rather than within the language and is typically described by a set of postulates, such as AGM postulates or KM postulates, that specify the properties of the new belief set based on the initial one and the new information acquired. To represent both higher-order beliefs and the belief change operation syntactically within the language, the doxastic modalities are typically supplied with more or less complex operators that describe belief change. This is the realm of dynamic epistemic logic that has roots in the public announcement logic of Plaza and later independent work by Gerbrandy–Groeneveld. What is missing from these approaches is a simple syntactic connection between the public announcement/new information and the change in beliefs. Since justification logic supplies a connection between static beliefs and the reasons for them, it is also natural to use it for describing beliefs that arise from public announcements. We present two systems of justification terms for public announcements that are not necessarily truthful and hence may lead to inconsistent beliefs. One system provides an explicit analog of Gerbrandy–Groeneweld's modal system of belief change, and the other is intended as an internalized version of the belief expansion operation. The benefit of both systems is that only a small number of additional justification operations is needed compared to those used to describe static beliefs. We also discuss the behavior of Moore-like sentences in both systems, i.e., sentences that in the modal case become false after being truthfully announced. 

Justification Logic is a relatively new field that studies provability, knowledge, and belief via proofs, or justifications, explicitly present in the language. Many justification logics have been developed that closely resemble modal epistemic logics of knowledge and belief with one important difference: instead of modality box with existential epistemic reading 'there exists a proof of F,' justification logics operate with constructs t : F, where a justification term t represents a blueprint of a Hilbert-style proof of F. The machinery of explicit justifications can be used to analyze well-known epistemic paradoxes such as Gettier's examples, to study self-referential properties of modal logics, and to avoid the Logical Omniscience Problem. This talk will focus on quantitative analysis of justification logics. We will give an overview of what is known about their decidability and complexity of the decision procedure, including most recent results. We will also analyze a realization procedure that provides a bridge from a modal epistemic logic to its justification counterpart. We will discuss the complexity of one such realization procedure as well as provide a qualitative analysis that leads to interesting corollaries about self-referentiality of modal logics.

The Logic of Proofs LP is an explicit counterpart of the modal logic S4, where modalities Box F, understood as "there is a proof for F," have been replaced by explicit propositions t:F, read as "t is a proof of F," for an appropriate system of proof terms t. LP naturally subsumes both typed lambda-calculus and modal logic. Artemov has offered an algorithm that recovered explicit proof terms in modalities in a given cut-free S4-derivation, thus, revealing a system of explicit proofs encoded in each S4-derivation. We modify this algorithm to produce explicit proofs whose lengths are polynomial in the size of the initial S4-derivation whereas the original algorithm gave an exponential blow-up. We also show that according to the explicit proofs semantics, the modal logic S4 encodes self-referential proofs, i.e. the ones where c:A(c) can occur.

The blending of syntactic and semantic methods through correspondence theory has provided both new generic ways of creating analytic cut-free calculi and a novel modular constructive method for proving interpolation properties in modal logics. We show that the two methods can be combined to the mutual benefit by demonstrating that the Craig and Lyndon interpolation properties (IPs) can be proved based on a labelled sequent calculus. We also provide sufficient criteria on the Kripke-frame characterization of a logic that guarantee the IPs. In particular, we show that classes of frames definable by quantifier-free Horn formulas correspond to logics with the IPs. These criteria capture the modal cube and the infinite family of transitive Geach logics.

The proof-theoretic method of proving the Craig interpolation property was recently extended from sequents to nested sequents and hypersequents. There the notations were formalism-specific, obscuring the underlying common idea, which is presented here in a general form applicable also to other similar formalisms, e.g., prefixed tableaus. It describes requirements sufficient for using the method on a proof system for a logic, as well as additional requirements for certain types of rules. The applicability of the method, however, does not imply its success. We also provide examples from common proof systems to highlight various types of interpolant manipulations that can be employed by the method. The new results are the application of the method to a recent formalism of grafted hypersequents (in their tableau version), the general treatment of external structural rules, including the analytic cut, and the method’s extension to the Lyndon interpolation property.

Artemov established an arithmetical interpretation for the Logics of Proofs LP(CS), which yields a classical provability semantics for the modal logic S4. These Logics of Proofs are parameterized by so-called constant specifications CS that state which axioms can be used in the reasoning process, and the arithmetical interpretation relies on the constant specifications being finite. In this paper, we remove this restriction by introducing weak arithmetical interpretations that are sound and complete for a wide class of constant specifications, including infinite ones. In particular, they interpret the full Logic of Proofs LP. 

Justification logic is an epistemic framework that provides a way to express explicit justifications for the agent's belief. In this paper, we present OPAL, a dynamic justification logic that includes term operators to reflect public announcements on the level of justifications. We create dynamic epistemic semantics for OPAL. We also elaborate on the relationship of dynamic justification logics to Gerbrandy–Groeneveld's PAL by providing a partial realization theorem.

The Logic of Proofs LP is an explicit counterpart of the modal logic S4, where modalities ▢F, understood as "there is a proof for F," have been replaced by explicit propositions t : F, read as "t is a proof of F," for an appropriate system of proof terms t. LP naturally subsumes both typed lambda-calculus and modal logic. Artemov has offered an algorithm that recovers explicit proof terms in modalities in a given cut-free S4-derivation, thus revealing a system of explicit proofs encoded in each S4-derivation. We modify this algorithm to produce explicit proofs whose lengths are polynomial in the size of the initial S4-derivation, whereas the original algorithm gave an exponential blow-up. We also show that according to the explicit proofs semantics, the modal logic S4 encodes self-referential proofs, i.e. the ones where c:A(c) can occur.

Explicit modal logic was introduced by S. Artemov in 1995. Whereas the traditional modal logic uses atoms "Box F" with a possible semantics "F is provable", the explicit modal logic deals with atoms of form t:F, where t is a proof polynomial denoting a specific proof of a formula F. Artemov found the explicit modal logic LP in this new format and built an algorithm that recovers explicit proof polynomials corresponding to modalities in every derivation in K. Goedel's modal provability calculus S4 (combined with the straightforward reading of proof polynomials as arithmetical proofs this provided an intended provability semantics for S4 and thus solved a problem left open by Goedel in 1933). In this paper we study the complexity of LP as well as the complexity of explicit counterparts of the modal logics K, D, T, K4, D4 found by V. Brezhnev. The main result: the satisfiability problem for each of these explicit modal logics belongs to the class Sigma_2 in the polynomial hierarchy. Similar problem for the original modal logics is known to be PSPACE-complete. Therefore, explicit modal logics have much better upper complexity bounds than the original modal logics.