Topic Archive: modal logic
This talk is on recent work with Joel Hamkins and Benedikt Loewe on ways in which finite-frame properties of specific modal logics can be combined with assertions in ZFC to show that these modal logics are related to those which arise from interpreting Gamma-forcing extensions of a model of ZFC as possible worlds of a Kripke model, where Gamma can be any of several classes of notions of forcing.
Modeling Intuitionistic Epistemic Logic via Provability and Verification (joint work with S. Artemov)
In 1933, Goedel offered a provability semantics for intuitionsitic logic IPC by means of a syntactical embedding of IPC into the modal logic S4 which Goedel considered a calculus for classical provability. Goedel’s embedding later became a key ingredient of the BHK-style semantics of classical proofs for intuitionsitic logic via the Logic of Proofs. We will establish the embedding/interpretation of Intuitionistic Epistemic Logic IEL into a natural extension (which we suggest calling S4V) of Goedel’s provability logic S4 by a verification modality. Basically, we will explain IEL via classical provability and verification coded in S4V the way Goedel explained intuitionistic logic via classical provability by interpreting it in S4.
Separation Logic is used as an assertion language for Hoare-style proof systems about programs with pointers, and there is an ongoing quest for understanding its complexity and expressive power. Alternatively, there are a lot of activities to develop verification methods with decision procedures for fragments of practical use.
Actually, there exist many versions or fragments of Separation Logic that can be viewed as fragments of Second-Order Logic, as well as variants of Modal or Temporal Logics in which models can be updated dynamically (as in Public Announcement Logic).
In this talk, after introducing first principles on Separation Logic, issues related to decidability, computational complexity and expressive power are discussed. We provide several tight relationships with Second-Order Logic, Interval Temporal Logic or Data Logics, depending on the variants of the logic and on the syntactic resources available.
Results presented during the talk span from standard ones about Separation Logic to more recent ones, some of them obtained in collaboration with Dr. Morgan Deters (NYU, CIMS).
Non-rigid designators play a major role in modal logics, when applied to aspects of natural language. Not only constants can be non-rigid, but also function symbols, and this is sometimes essential. I will discuss some examples, formalize them, and provide a semantics. If time permits, I will also present a nested sequent proof system to go with all this.
The complexity of Modal Logic has been extensively studied. Ladner has established most of what are now considered classical results on the matter, determining that most of the usual modal logics are PSPACE-complete. Furthermore, as Chagrov and Rybakov showed, some of these logics remain PSPACE-complete even for their variable-free fragments. We present parameters of modal formulas whose effect on the complexity of modal logic has been studied – like modal depth – and we identify sources of complexity for modal satisfiability.
A big part of this talk is joint work with Michael Lampis and Valia Mitsou.
In this lecture we will review topological models of modal and justification logics.
We will introduce a new, slightly more general class of models for Justification Logic and compare them with Mkrtychev, Fitting, and modular models. Completeness Theorem will be established, examples will be given and plausible areas of applications outlined.
This will be a mostly survey talk in which we discuss a variety of models for Justification Logic: arithmetical models (Goedel, Artemov), Mkrtychev models, Fitting models, topological models (Artemov, Nogina), modular models (Artemov), Sedlar’s group models, and some others. We will continue discussing applications.
This talk continues my previous one from October 22. In that, I gave justification counterparts for S4.2 and for K4^3, possible world justification semantics, and a completeness proof. The completeness proof used a canonical model construction. Now I’l use that canonical model to prove, non-constructively, realization theorems for the two logics. The methodology is the same as in a paper of mine published in 2005, though the presentation has change somewhat. Primarily my motivation is to explore the range of modal logics having justification counterparts—to discover its extent and limits.
In this talk we give a computationally motivated presentation of J-Calc. J-Calc is an extension of simply typed lambda calculus with justifications and justified modal types.
Initiating from textbook examples of modular programs, we will present the modal type theory of J-Calc as a type system corresponding to programming with modular definitions. More specifically, we will show how justified modality offers a logical reading to separate compilation in modular functional programming.
Possible world semantics was introduced for justification logic in 2005. Initially it was for the Logic of Proofs, but it quickly extended to “nearby” logics, and more slowly to a wider family. Eight years is a long time, and by now people may be generally familiar with the ideas without having gone through any of the details. I will try to remedy that.
Long before Kripke semantics became standard in modal logic, Tarski showed us that the basic propositional modal language can be interpreted in topological spaces. In Tarski’s semantics for the modal logic $S4$, each propositional variable is evaluated to an arbitrary subset of a fixed topological space. I develop a related, measure theoretic semantics, in which modal formulas are interpreted in the Lebesgue measure algebra, or algebra of Borel subsets of the real interval $[0,1]$, modulo sets of measure zero. This semantics was introduced by Dana Scott in the last several years. I discuss some of my own completeness results, and ways of extending the semantics to more complex modal languages.