Blog Archives

Topic Archive: modal logic

Heinrich Wansing
Ruhr University Bochum
Prof. Dr. Wansing (M.A. Phil., Free University of Berlin, 1988; D. Phil., Free University of Berlin, 1992; Habilitation in Logic and Analytical Philosophy, University of Leipzig, 1997) is Professor of Logic and Epistemology at the Ruhr University Bochum, and conducts research in philosophical logic, modal logic, non-classical logic and epistemology.
Set theory seminarFriday, April 11, 201410:00 amGC6417

George Leibman

Structural Connections Between a Forcing Class and its Modal Logic

Bronx Community College, CUNY

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.

Computational Logic SeminarTuesday, April 8, 20142:00 pmGraduate Center, rm. 3209.

Tudor Protopopescu

Modeling Intuitionistic Epistemic Logic via Provability and Verification (joint work with S. Artemov)

CUNY Graduate Center

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.

Computational Logic SeminarTuesday, March 18, 20142:00 pmGraduate Center, rm. 3209

Stéphane Demri

Separation Logic and Friends

NYU & CNRS, France

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).

Computational Logic SeminarTuesday, March 11, 20142:00 pmGraduate Center, rm. 3209

Melvin Fitting

Height and Happiness

Lehman College - CUNY Graduate Center

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.

Computational Logic SeminarTuesday, March 4, 20141:00 pmGraduate Center, rm. 8405New room, for this talk only!

Antonis Achilleos

Parameters and the Complexity of Modal Satisfiability

Graduate Center CUNY

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.

Computational Logic SeminarTuesday, February 18, 20142:00 pmGraduate Center, rm. 3209

Sergei Artemov

Models of Justification Logic III

The CUNY Graduate Center

In this lecture we will review topological models of modal and justification logics.

Computational Logic SeminarTuesday, February 11, 20142:00 pmGraduate Center, room 3209

Sergei Artemov

On Models of Justification Logic II.

The CUNY Graduate Center

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.

Computational Logic SeminarTuesday, February 4, 20142:00 amGraduate Center, room 3209

Sergei Artemov

On models of Justification Logic

The CUNY Graduate Center

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.

Computational Logic SeminarTuesday, November 12, 20132:00 pmGraduate Center, rm. 3209

Melvin Fitting

Realization Semantically

Lehman College - CUNY Graduate Center

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.

Computational Logic SeminarTuesday, October 29, 20132:00 pmGraduate Center, rm. 3209

Konstantinos Pouliasis

J-Calc: Justified Modal Types and Functional Programs

Graduate Center CUNY

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.

Computational Logic SeminarTuesday, October 22, 20132:00 pmGraduate Center, rm, 3209

Melvin Fitting

Justification Logic Semantics: A Little New, but Mostly Old

Lehman College - CUNY Graduate Center

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.

CUNY Logic WorkshopFriday, November 22, 20132:00 pmGC 6417

Tamar Lando

Measure semantics for modal logics

Columbia University

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.

Hitoshi Omori
Kobe University, Visiting Fellow, Grad Center, CUNY
Hitoshi Omori is a visting fellow in the CUNY Graduate Center program in Philosophy, visiting from Kobe University. His main research interests are Logic, Logic And Foundations Of Mathematics, Philosophy of Logic, Philosophical Logic, Modal Logic and Non-Classical Logic.