# Computational Logic Seminar

The seminar in computational logic at the CUNY Graduate Center
(81 items)

Computational Logic SeminarThursday, September 29, 20164:00 pmGraduate Center, rm. 8400

# The unreasonable effectiveness of Nonstandard Analysis.

Department of Mathematics, Ghent University

Nonstandard Analysis (NSA) was introduced around 1965 by Robinson as a formalization of the intuitive infinitesimal calculus which is in use to date in most of physics and historically in mathematics until the advent of Weierstrass’ epsilon-delta framework. Famous people like Connes and Bishop have derided NSA for its alleged utter lack of computational/effective/constructive content. In this talk I show that every theorem of ‘pure’ NSA can be (equivalently) converted to a theorem of computable mathematics. In many cases, the resulting theorem is even constructive in the sense of Bishop.

Computational Logic SeminarTuesday, May 10, 20162:00 pmGraduate Center, rm. 4422

Delft University of Technology

The present talk reports on some recent developments in the mathematical theory of epistemic updates, a very fruitful line of research initiated in [4, 3] and further pursued in [2, 5, 1]. This line of research is motivated by the observations that ‘dynamic phenomena’ are independent of their underlying static logic being classical, and that this assumption is unrealistic in many important contexts; for instance, in all those contexts (such as scientific experiments, acquisition of legal evidence, verification of programs, etc.) where the notion of truth is procedural. Desirable and conceptually important as it is, the more general problem of identifying the right intuitionistic (or more generally nonclassical) counterparts of (modal-like) expansions of classical logic (such as modal logics themselves, or hybrid logics, etc.) has proven to be difficult, and for most of these logics, this question is still open. Indeed, different axiomatizations which in the presence of classical tautologies define the same logic become nonequivalent against a weaker propositional background. Hence, each classical axiomatization might have infinitely many nonequivalent nonclassical potential counterparts. We introduce a uniform methodology for defining the nonclassical counterparts of dynamic logics, which is grounded on semantics rather than on syntax. This methodology is based on the dual characterizations of the transformations of models which interpret the actions. This dual characterization makes it possible to define epistemic updates on algebras, thanks to which an algebraic semantics for (e.g.) the intuitionistic counterpart of Baltag-Moss-Solecki’s dynamic epistemic logic can be defined e.g. on Heyting algebras.

References
[1] Z. Bakhtiari, U. Rivieccio. Epistemic Updates on Bilattices. Proceedings of the Fifth International Workshop on Logic, Rationality and Interaction – LORI, LNCS 9394, pp. 426-8 (2015).
[2] W. Conradie, S. Frittella, A. Palmigiano, A. Tzimoulis, Probabilistic Epistemic Updates on Algebras, Proceedings of the Fifth International Workshop on Logic, Rationality and Interaction – LORI, LNCS 9394, pp. 64-76 (2015).
[3] Alexander Kurz and Alessandra Palmigiano. Epistemic updates on algebras. Logical Methods in Computer Science, 2013. arXiv:1307.0417. 1
[4] Minghui Ma, Alessandra Palmigiano, and Mehrnoosh Sadrzadeh. Algebraic semantics and model completeness for intuitionistic public announcement logic. Annals of Pure and Applied Logic, 165 (2014) 963-995.
[5] U. Rivieccio, Bilattice Public Announcement Logic, Proc. AiML 10 (2014).

Computational Logic SeminarTuesday, May 3, 20162:00 pmGraduate Center, rm. 4422

# Some abstract versions of Goedel’s Second Incompleteness Theorem based on non-classical logics

Steklov Mathematical Institute of Russian Academy of Sciences in Moscow

We study abstract versions of Goedel’s second incompleteness theorem and formulate generalizations of Loeb’s derivability conditions that work for logics weaker than the classical one. We isolate the role of the contraction and weakening rules in Goedel’s theorem and give a (toy) example of a system based on modal logic without contraction invalidating Goedel’s argument. On the other hand, Goedel’s theorem is established for a version of Peano arithmetic without contraction. (Joint work with Daniyar Shamkanov)

Computational Logic SeminarTuesday, April 19, 20162:00 pmGraduate Center, rm. 4422

# Dark Matter of Epistemology

We have already shown that only deductively complete epistemic scenarios admit traditional single-model characterizations. In this talk we show that the paradigmatic Muddy Children story is deductively complete and fairly represented by its standard Kripke model. However, the whole variety of its modifications with partial knowledge, asymmetric knowledge, etc., are not deductively complete and hence are invisible “Dark Matter” from the traditional single-model perspective. We show several examples of such “invisible” scenarios that admit natural syntactic analysis and resolution. Finally, we will discuss a version of Muddy Children, in which justifications become a key ingredient of the solution. These examples represent, in a nutshell, the corresponding classes of real world epistemic problems which lie off limits of the traditional single-model analysis but can be analyzed by a proper combination of syntactic and semantic methods.

Computational Logic SeminarTuesday, April 12, 20162:00 pmGraduate Center, rm. 4422

# Epistemic Model Theory revisited II.

We provide a brief but rigorous review of the model theory for modal epistemic logic. In addition to the classical soundness and completeness results we will focus on features that are normally left hidden: necessitation in epistemic scenarios, internalization property of the model, knowledge of the model, etc. This should provide a solid base for further epistemic logic investigations.

In this talk, we take a fresh look at canonical models of the usual multi-modal systems, and discuss what they can and cannot do in the epistemic settings.

Computational Logic SeminarTuesday, April 5, 20162:00 pmGraduate Center, rm. 4422

# Gödel/Artemov-Style Analyses for Variants of Intuitionistic Logic

CUNY Graduate Center, Department of Philosophy

Kurt Gödel’s provability interpretation of intuitionistic logic and Sergei Artemov’s Logic of Proofs (LP) have jointly shed a great deal of light on the inner machinery of intuitionistic logic. In this talk, I will give Gödel/Artemov-style analyses to several variants of intuitionistic logic: Cecylia Rauszer’s Heyting-Brouwer Logic (HB) and David Nelson’s Logics of Constructible Falsity (N3 and N4). Heinrich Wansing has sketched out Gödel-style provability interpretations of these systems by distinguishing between categories of justification, e.g., proof and refutation. I will show that identifying these categories with distinct agents in Tatyana Yavorskaya-Sidon’s two-agent Logic of Proofs LP^2 permits salient Gödel/Artemov-style translations of HB and N3 into extensions of LP^2. Finally, we will discuss the prospects for a similar analysis of N4, considering proposals of Melvin Fitting and Che-Ping Su and a conjecture concerning a translation of N4 into the modal logic S4.

Computational Logic SeminarTuesday, March 29, 20162:00 pmGraduate Center, rm. 4422

# Towards Paraconsistent Game Theory

Department of Computer Science, University of Bath, England

In this programmatic talk, I will talk about three major examples of paraconsistency and paradoxes in games. Paraconsistent logic is a family of non-classical logics in which contradictions do not entail everything. In this talk, first, I will discuss game theoretical semantics for paraconsistent logic and observe how semantic games change in different, especially in paraconsistent logics. Then, I will consider a self-referential paradox of epistemic game theory, called Brandenburger-Keisler Paradox, and present a model for it. Following, I will shift my attention non-self-referential paradoxes and suggest a non-self-referential paradox in games. These three major cases, I will argue, will be a call for the necessity of the use of non-classical logics in game theoretical reasoning.

Computational Logic SeminarTuesday, March 22, 20162:00 pmGraduate Center, rm. 4422

# Epistemic Model Theory revisited.

We provide a brief but rigorous review of the model theory for modal epistemic logic. In addition to the classical soundness and completeness results we will focus on features that are normally left hidden: necessitation in epistemic scenarios, internalization property of the model, knowledge of the model, etc. This should provide a solid base for further epistemic logic investigations.

Computational Logic SeminarTuesday, March 15, 20162:00 pmGraduate Center, rm. 4422

# Does knowledge of the model matter?

As we have already discussed, the traditional epistemic reading of Kripke models relies on the hidden assumption of the knowledge of the model by the agent. In the multi-agent setting, e.g. in Epistemic Game Theory, this becomes the assumption of the common knowledge of the model, which is not regarded realistic, and often is theoretically impossible. We sketch logician’s recommendations of how to handle epistemic scenarios without relying on common knowledge of the model.

Computational Logic SeminarTuesday, March 8, 20162:00 pmGraduate Center, rm. 4422

# Justification Epistemic Models: technical details.

We will provide exact definitions and a rigorous formal treatment of justification epistemic models (JEM). The JEM for Russell’s prime minister example will be presented with all details.

Computational Logic SeminarTuesday, March 1, 20162:00 pmGraduate Center, rm. 4422

# How (Not) To Aggregate Normative Reasons

Pisa-Florence/NYU/EPHE

Justification logic can be used to make sense of deontic modality, where justification terms are interpreted as normative reasons. Unlike proofs or epistemic evidence, which are (generally) factive, normative reasons must be ordered, since arguably one only ought to do just what one has most (more, stronger, etc) reason to do.

I make precise in what sense normative reasons are scalar, why an aggregation operation is needed, and introduce the most common types of scales. I then show that normative reasons cannot be (numerically) measured, and that the scale of normative reasons, if any, is therefore not ratio, interval, or ordinal (in a precise measurement-theoretic sense). I eventually discuss the consequences of these results for normative theorizing, and especially for normative particularism.

Computational Logic SeminarTuesday, February 23, 20162:00 pmGraduate Center, rm. 4422

# Paraconsistent logic, evidence, and justification

Lehman College - CUNY Graduate Center

In a forthcoming paper, Walter Carnielli and Abilio Rodriguez propose a Basic Logic of Evidence (BLE) whose natural deduction rules are thought of as preserving evidence instead of truth. BLE turns out to be equivalent to Nelson’s paraconsistent logic N4, resulting from adding strong negation to Intuitionistic logic without Intuitionistic negation. The Carnielli/Rodriguez understanding of evidence is informal. We provide a formal alternative, using justification logic. First we introduce a modal logic, KX4, in which box-X can be read as asserting there is implicit evidence for X, where we understand evidence to permit contradictions. We show BLE embeds into KX4 in the same way that Intuitionistic logic embeds into S4. Then we formulate a new justification logic, JX4, in which the implicit evidence motivating KX4 is made explicit. KX4 embeds into JX4 via a realization theorem. Thus BLE has both implicit and explicit evidence interpretations in a formal sense.

Computational Logic SeminarTuesday, February 2, 20162:00 pmGraduate Center, rm . 4422

# Evidence-based epistemic models

We will survey the standard modal logic approach to model the “knowledge vs justified true belief” scenarios, in particular its recent account in Williamson, Timothy “A note on Gettier cases in epistemic logic” Philosophical Studies 172.1 (2015): 129-140. We argue that the “old school” approach by Williamson to model justified belief as a modality without going deeper to the level of individual justifications is rather limited. Whereas it indeed suffices to satisfactory treat Gettier examples with a unique justification in the picture, it fails even on simplest examples with more than one justification, e.g., Russell’s Prime Minister Example. On the constructive side, we offer a principled way to building epistemic models entirely from systems of justifications; standard epistemic models are special cases of these evidence-based epistemic models. New models cover wide range of epistemic scenarios, including Russell’s example, in a natural way.

Computational Logic SeminarTuesday, December 8, 20152:00 pmGraduate Center, room 3309

# Justification Logic and Aggregating Probabilistic Evidence

Evidence aggregation is a well-known problem which appears naturally in many areas. A classical approach to this problem is via Bayesian probabilistic evidence aggregation. Our approach is radically different. We consider the following situation: suppose a proposition X logically follows from a database — a set of propositions D which are supported by some known evidence, vector u of events in a probability space. We answer the question of what is the best aggregated evidence for X justified by the given data. We show that such aggregated evidence e(u) could be assembled algorithmically from the collection of all logical derivations of X from D. This approach can handle conflicting and inconsistent data and allows the gathering both positive and negative evidence for the same proposition. The problem is formalized in a version of justification logic and the conclusions are supported by corresponding completeness theorems.

Computational Logic SeminarTuesday, December 1, 20152:00 pmGraduate Center, rm. 3309

# An Arithmetical Interpretation of Verification and Intuitionistic Knowledge

Intuitionistic epistemic logic, IEL, introduces to intuitionistic logic an epistemic operator which reflects the intended BHK semantics of intuitionism. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the Logic of Proofs, LP, and its arithmetical semantics. We show here that the Gödel embedding, realization, and an arithmetical interpretation can all be extended to S4 and LP extended with a verification modality, thereby providing intuitionistic epistemic logic with an arithmetical semantics too.

Computational Logic SeminarTuesday, May 12, 20152:00 pmGraduate Center, rm. 6421

# Intuitionistic Analysis of Russell and Gettier Examples

Intuitionistic truth is proof-based, and intuitionistic knowledge is the result of verification. The corresponding logic IEL of intuitionistic knowledge (Artemov and Protopopescu, 2014) has offered a principled resolution of the Fitch-Church knowability paradox. In this talk we will analyze paradigmatic Russell and Gettier examples from intuitionistic epistemic positions, both informally, and formally within proper versions of IEL.

Time permitting, we will discuss the list of possible research projects.

Computational Logic SeminarTuesday, May 5, 20152:00 pmGraduate Center, rm. 6421

# Epistemic Considerations on Extensive-Form Games

In this talk, we discuss several topics in extensive-form games. First, we consider perfect information games with belief revision with players who are tolerant of each other’s “hypothetical” errors. Second, we study imperfect information games with players who have no way of assigning probabilities to various possible outcomes, and we analyze how players might choose in such games. We then look into how a truthful manipulator whose motives are not known to players can create a certain knowledge situation about a game, and change the way the game will be played.

Computational Logic SeminarTuesday, April 28, 20152:00 pmGraduate Center, rm. 6421

# Syntactic View of Strategic Games

We suggest an epistemic logic analysis of strategic games with ordinal payoffs, including Nash’s justification of the equilibrium solution concept: the solution is derived by the players from the game description. We show that most of the classes of games do not have Nash solutions, and for those that have, stronger solution concepts (e.g, domination) and/or refinements of Aumann rationality are needed.

Computational Logic SeminarTuesday, April 21, 20152:00 pmGraduate Center, rm. 6421

# A general completeness theorem relating sequents and bivaluations

Federal University of Rio de Janeiro, Brazil

In this talk I will present a theorem justifying an intuitive semantical interpretation of rules of sequent proof systems. This theorem is based on the one hand on a generalization of Lindenbuam maximalization theorem and on the other hand on a general semantical theory of bivaluations, not necessarily truth-functional, originally developed by Newton da Costa for paraconsistent systems. I will show that this theorem gives a better understanding of sequent calculus and that it can fruitfully be applied to a wide class of logical systems providing instantaneous completeness results. This is a typical example of work in the line of the universal logic project, of which I will say a few words.

Reference: Logica Universalis, Special Double Issue – Scope of Logic Theorems. Volume 8, Issue 3-4, December 2014.

Computational Logic SeminarTuesday, April 14, 20152:00 pmGraduate Center, rm. 6421

# Cut-Free Proofs for More and More Logics

Lehman College - CUNY Graduate Center

Gentzen introduced cut-free proofs in 1934. In these, all formulas are subformulas of what is being proved (and with the same polarity). This is an important feature for many reasons, proof search among them. In 1957 Ohnishi and Matsumoto extended Gentzen’s ideas to several modal logics. Beth introduced tableaus in the 1950’s, with their modern version coming from Smullyan in the 1960’s. Roughly, tableaus are sequent calculi upside-down. I (probably) introduced tableau versions of Ohnishi and Matsumoto’s calculi in the 1970’s. All this treated a small number of modal logics.

Based on an idea of Fitch, I introduced prefixed tableaus in 1972. These add new machinery, but are able to handle many more modal logics. Today they are rather common in automated theorem proving.

In a recent (yet unpublished) paper I introduced set prefixed tableaus. We now have machinery that can handle an infinite family of modal logics, including all the most common ones. And they do this in a uniform way, separating logical rules from so-called structural rules.

The idea that tableaus and sequent calculi are dual to each other continues. Nested sequents have been much studied. In a paper from 2012 I showed that nested sequents and prefixed tableaus were dual, in this sense. And I have a new construct, indexed nested sequents, which is dual to set prefixed tableaus. The pattern continues.

I will cover as much of this as time permits. (My talk is intended to be a trial run for a talk to be given at UNILOG, In Istanbul, this summer.)

Computational Logic SeminarTuesday, March 31, 20152:00 pmGraduate Center, 6421

# NEXP-completeness and Universal Hardness Results for Justification Logic

We provide a lower complexity bound for the satisfiability problem of a multi-agent justification logic, establishing that there are certain NEXP-complete multi-agent justification logics with interactions. We then use a simple modification of the corresponding reduction to prove that satisfiability for all multi-agent justification logics in a general class we consider is $Sigma_2^p$-hard — given certain reasonable conditions. Our methods improve on these required conditions for the same lower bound for the single-agent justification logics, proven by Buss and Kuznets in 2009, thus answering one of their open questions.

http://arxiv.org/abs/1503.00362

Computational Logic SeminarTuesday, March 24, 20152:00 pmGraduate Center, room 6421

# Bi-simulation of epistemic structures: a semantic proof of completeness for Muddy Children Puzzle.

In this talk we discuss truth preserving bi-simulations of multi-agent Kripke models. As an application, we present a semantic proof of the completeness of the syntactic formulation of Muddy Children Puzzle with respect to its standard model.

Computational Logic SeminarTuesday, March 17, 20152:00 pmGraduate Center, room 6421

Lehman College - CUNY Graduate Center

A mixture of propositional dynamic logic and epistemic logic that we call PDL + E is used to give a formalization of Artemov’s knowledge based reasoning approach to game theory. Epistemic states of players are represented explicitly and reasoned about formally. We give a detailed analysis of the Centipede game using both syntactic proofs and semantical arguments. Formal proofs are used establish what is the case and what is needed to show this. Semantical machinery is used to establish what cannot be the case. All this makes a case that PDL + E can be a useful basis for the logical investigation of game theory.

Computational Logic SeminarTuesday, March 10, 20152:00 pmGraduate Center 6421

# Syntactic Epistemic Logic and Games IV

In this talk we consider knowledge structures used to model epistemic components of extensive-form games. We show that the traditional semantic mode of specification by a single model cannot capture some natural epistemic notions, e.g., mutual knowledge of rationality, used in Epistemic Game Theory. In contrast, Syntactic Epistemic Logic handles this and many other conditions that lie outside the scope of the semantic tradition. We outline general principles of Syntactic Epistemic Logic in connection to Game Theory.

Computational Logic SeminarTuesday, March 3, 20152:00 pmGraduate Center 6421

# Syntactic Epistemic Logic and Games III

We discuss the Muddy Children puzzle MC, identify and fix the gap in its solution: a completeness analysis is required if the problem is specified syntactically, but analyzed by reasoning on a specific model. We show that the syntactic description of MC is complete w.r.t. its model used in the standard solution. We will present two proofs of completeness: syntactic, by induction on a formulas, and semantic, which makes use of bounded morphisms, a special case of bisimulations. We then present a modification of MC, MClite, and show that it is not deductively complete, has no semantic characterization and cannot be handled by traditional semantic methods. We give a syntactic solution of MClite.

Time permitting, we will venture further into extensive games and their epistemic models

Computational Logic SeminarTuesday, February 24, 20152:00 pmGraduate Center 6421

# Syntactic Epistemic Logic and Games II

The Syntactic Epistemic Logic, SEL, suggests making the syntactic formalization of an epistemic scenario its formal specification. Since SEL accommodates constructive model reasoning, we speak about extending the scope of formal epistemology. SEL offers a cure for two principal weaknesses of the traditional semantic approach.
1. The traditional semantic approach in epistemology covers only deductively complete scenarios in which all epistemic assertions of any depth are specified. However, intuitively, “most” of epistemic scenarios are not complete. SEL suggests a way to handle incomplete scenarios with reasonable syntactic descriptions.
2. In addition, SEL seals the conceptual and technical gap, identified by R. Aumann, between the syntactic character of game descriptions and the semantic method of analyzing games.

Computational Logic SeminarTuesday, February 17, 20152:00 pmGraduate Center 6421

# Syntactic Epistemic Logic and Games I

We argue that the traditional way to specify an epistemic situation via a single model is unnecessarily restrictive: there are numerous scenarios which do not have conventional single-model characterizations: less-than-common knowledge (e.g., mutual knowledge), partial, asymmetric knowledge, etc. Syntactic Epistemic Logic, SEL, suggests a way out of this predicament by viewing an epistemic scenario as specified syntactically by a set of formulas which corresponds to the characterization via a class of models rather than a single model. In addition, in Game Theory, SEL helps to seal the conceptual and technical gap, identified by R.Aumann, between the syntactic character of game descriptions and the predominantly semantical way of analyzing games.

This will be the first in the series of talks on SEL. We will consider natural examples of epistemic or game theoretic scenarios which have manageable syntactic description but do not have acceptable single model characterizations.

Computational Logic SeminarTuesday, February 10, 20152:00 pmGraduate Center rm. 6421

# First-order justification logic JT45

University of São Paulo

Among the different propositional justification logics, JT45 is the justification counterpart of the modal logic S5. Although there is a growing literature about propositional justification logic, there are only a few papers about the first-order version of justification logic. And most of those papers focus on the first-order version of LP. The goal of this talk is to present a first approach to first-order JT45 (FOJT45). Using Fitting models we will present a possible worlds semantics for FOJT45 and with that establish a Completeness Theorem. We will also discuss some topics related to first-order modal logic such as the Barcan Formula and the failure of the Interpolation Theorem.

Computational Logic SeminarTuesday, February 3, 20152:00 pmGraduate Center 3307

# What is Constructive Axiomatic Method?

Institute of Philosophy of Russian Academy of Sciences; Smolny College of Liberal Arts and Sciences, Saint-Petersburg State University

The received notion of axiomatic theory, which stems from Hilbert, is that of set T of propositions (either contentful or non-interpreted aka propositional forms) with subset A of axioms provided with a notion of consequence, which generates T from A in the obvious way. I argue that this standard notion is too narrow for being an adequate theoretical model of many mathematical theories; the class of such counter-examples is apparently very large and it includes such different theories as the geometrical theory of Euclid’s Elements, Book 1, and the more recent Homotopy type theory. In order to fix this problem I introduce a more general notion of theory, which uses typing and a generalized notion of consequence applicable also to objects of other types than propositions. I call such a theory constructive axiomatic theory and show that this particular conception of being constructive indeed captures many important ideas concerning the mathematical constructivity found in the earlier literature from Hilbert to Kolmogorov to Martin-Lof. Finally I provide an epistemological argument intended to show that the notion of constructive axiomatic theory is more apt to be useful in natural sciences and other empirical contexts than the standard notion. Disclaimer: The notion of constructive axiomatic theory is not my invention. The idea and its technical implementation are found in Martin-Lof ‘s constructive type theory if not already in Euclid. My aim is to make this notion explicit and introduce it into the continuing discussions on axiomatic method and mathematical and logical constructivity.

Computational Logic SeminarTuesday, May 13, 20142:00 pmGraduate Center, rm. 3209

# What ‘If’?

CUNY Graduate Center, Ph.D. Program in Philosophy

Solutions to the paradoxes of semantic self-reference which endorse the unrestricted T-schema (and cognate principles) normally assume that the conditional involved in the schema is a detachable one (i.e., one that satisfies modus ponens). In a paraconsistent setting, there is another possibility: to take it to be the material conditional. In this talk, I will discuss some of the ramifications of this possibility.

Computational Logic SeminarTuesday, May 6, 20142:00 pmGraduate Center, rm. 3209

# Paraconsistent Justification Logic (II): Quasi-Realization Theorem

The University of Melbourne

Paraconsistent justification logics are justification logic systems for inconsistent beliefs or commitments. In other words, these systems are intended to model the agent’s justification structure, when she has inconsistent beliefs or commitments.

Realization theorem is one important meta-theorem in the discourse of justification logic. Quasi-realization theorem can be taken to be a major step toward proving realization theorem. In the last semester, I introduced one paraconsistent justification logic, called PJ_b. The main focus of the talk on the coming Tuesday is quasi-realization. It will be proved that quasi-realization theorem – which holds for standard justification logic systems – also holds for PJ_b.

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

# Unified Logics

Chief Information Officer of Metropolitan Telecommunications, New York

The presentation studies the propositional logical systems containing multiple-conclusion rules that admit the asserted and rejected propositions at the same time.

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

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

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

# On non-self-referential realizable fragments

Given the known fact that realizations of modal logics T, K4, S4, and intuitionistic propositional logic IPC (via S4) each requires justification formula that is self-referential, it is reasonable to consider the fragment of each that can be realized non-self-referentially, called the non-self-referential realizable (NSR) fragment. Based on prehistoric graphs of G3-style sequent proofs of modal theorems, we are able to define the loop-free-provable (LFP) fragment of each logic that turns out to be a decidable subset of the NSR fragment. In this talk, we will explore properties of LFP fragments, their applications in the study of NSR fragments, and other related issues.

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

# 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

# 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!

# Parameters and the Complexity of Modal Satisfiability

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 25, 20142:00 pmCUNY Graduate Center, rm. 3209

# From Intuitionistic Epistemic Logic to a constructive resolution of the Knowability Paradox (joint work with S. Artemov)

We outline an intuitionistic view of knowledge which maintains the Brouwer-Heyting-Kolmogorov semantics and is consistent with Williamson’s suggestion that intuitionistic knowledge be regarded as the result of verification. We argue that on this view A -> KA is valid and KA -> A is not. We show the latter is a distinctly classical principle, too strong as the intuitionistic truth condition for knowledge which can be more adequately expressed by other modal means, e.g. ~(KA & ~A) “false is not known.” We construct a system of intuitionistic epistemic logic, IEL, codifying this view of knowledge and prove the standard meta-theorems for it. From this it follows that previous outlines of intuitionistic knowledge, responding to the knowability paradox, are insufficiently intuitionistic; by endorsing KA -> A they implicitly adopt a classical view of knowledge, by rejecting A -> KA they reject the constructivity of truth. Within the framework of IEL, the knowability paradox is resolved in a constructive manner which, as we hope, reflects its intrinsic meaning.

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

# Models of Justification Logic III

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

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

# On Models of Justification Logic II.

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

# On models of Justification Logic

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, January 28, 20142:00 pmGraduate Center, rm. 3209