Linear Logic, introduced by Girard ([Gir] 1987), is a kind of resource sensitive logic, since it lacks general forms of structural inferences. However, it restores controlled uses of structural inferences by its exponentials, which behaves like the S4 modality. In the usual resource semantics for Linear Logic, the formulas with exponentials are interpreted to mean the inexhaustibility of a resource. We study an extension of Linear Logic by relaxing the exponentials to the S5 type modality. Then, it is interpreted to mean the inexhaustibility and transferability of a resource. We show some basic properties of this logic: completeness, cut-eliminatbility, decidability. Also, we provide the realizability of our logic via Logic of proofs (aka, Justification Logic), introduced by Artemov [Art1, Art2].

This work is a continuation of our on-going research project with Professor Kurokawa on ’synthesizing substructural logics and logics of proofs’, including [KK], 2013.

References

[Art1] S. N. Artemov, Explicit provability and constructive semantics, Bulletin of Symbolic Logic 7(1), pp.1–36, 2001.

[Art2] S. N. Artemov, The Logic of Justification, Review of Symbolic Logic, 1(4), pp. 477-513, 2008.

[Gir] J. Girard, Linear Logic, Theoretical Computer Science 50, pp. 1–102, 1987.

[KK] H. Kurokawa and H. Kushida, Substructural Logic of Proofs, WoLLIC 2013: Logic, Language, Information, and Computation, LNCS 8071, pp.194-210, 2013.

Kripke models provide a versatile semantical tool in modal logic. It appears that when Kripkean methods were adopted in formal epistemology “as is” a key hidden assumption has been overlooked: the very truth condition of a knowledge assertion presupposes that the model itself is common knowledge among the agents. Naturally, this covers only well-controlled epistemic scenarios and leaves off scope numerous situations with partial/asymmetric knowledge. In this talk, we
1) offer a theory of sub-Kripkean epistemic models for unimodal logics;
2) discuss research directions for multi-agent cases.

Proofs and justification are gradually making their way from meta-logical notions into the formal logic itself and becoming mathematical logical objects. This makes the logic language (much) more precise and connects the logic apparatus to numerous new areas of interest.

Part III: Possible worlds with and without modalities. More epistemic examples. Open questions and research projects.

Proofs and justification are gradually making their way from meta-logical notions into the formal logic itself and becoming mathematical logical objects. This makes the logic language (much) more precise and connects the logic apparatus to numerous new areas of interest.

Part I: we describe a generic logical semantics of justifications within the classical truth values logic framework: justifications here appear as sets of formulas with appropriate closure conditions.

Part II: introducing possible worlds.

Proofs and justification are gradually making their way from meta-logical notions into the formal logic itself and becoming mathematical logical objects. This makes the logic language (much) more precise and connects the logic apparatus to numerous new areas of interest. In this talk, we describe a generic logical semantics of justifications within the classical truth values logic framework: justifications here appear as sets of formulas with appropriate closure conditions.

We consider the fragment of propositional multi-modal logic that consists of implications whose premise and conclusion are strictly positive (SP) modal formulas constructed from propositional variables using conjunction and unary diamond operators. SP-logics can be interpreted over bounded meet-semilattices with normal monotone operators (SLOs, for short), and over first-order structures (aka Kripke frames). The former interpretation provides natural calculi for SP-logics, while reasoning over the latter can be supported by modern provers and description logic reasoners, and is often tractable. An SP-logic is called (Kripke) complete if it has the same consequences in each of these semantics. This talk reports on our first steps in developing completeness theory for SP-logics, which turns out to be quite different from classical completeness theory for modal logics. We also consider some related problems, in particular, axiomatisability and computational complexity.

In analogy with the ancient views on potential as opposed to actual infinity, set-theoretic potentialism is the philosophical position holding that the universe of set theory is never fully completed, but rather has a potential character, with greater parts of it becoming known to us as it unfolds. In this talk, I should like to undertake a mathematical analysis of the modal commitments of various specific natural accounts of set-theoretic potentialism. After developing a general model-theoretic framework for potentialism and describing how the corresponding modal validities are revealed by certain types of control statements, which we call buttons, switches, dials and ratchets, I apply this analysis to the case of set-theoretic potentialism, including the modalities of true-in-all-larger-V_β, true-in-all-transitive-sets, true-in-all-Grothendieck-Zermelo-universes, true-in-all-countable-transitive-models and others. Broadly speaking, the height-potentialist systems generally validate exactly S4.3 and the height-and-width-potentialist systems generally validate exactly S4.2. Each potentialist system gives rise to a natural accompanying maximality principle, which occurs when S5 is valid at a world, so that every possibly necessary statement is already true.  For example, a Grothendieck-Zermelo universe V_κ, with κ inaccessible, exhibits the maximality principle with respect to assertions in the language of set theory using parameters from V_κ just in case κ is a Σ₃-reflecting cardinal, and it exhibits the maximality principle with respect to assertions in the potentialist language of set theory with parameters just in case it is fully reflecting V_κ < V.

This is current joint work with Øystein Linnebo, in progress, which builds on some of my prior work with George Leibman and Benedikt Löwe in the modal logic of forcing. Comments and questions can be made on the speaker’s blog.

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)

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

Gödel inaugurated a project of finding an arithmetic semantics for intuitionistic logic, but did not complete it. It was finished by Sergei Artemov, in the 1990’s. As part of this work, Artemov introduced the first justification logic, LP, (standing for logic of proofs). This is a propositional modal-like logic, with an infinite family of proof or justification terms, and can be seen as an explicit version of the well-known modal logic S4. There is a possible world semantics for LP (due to me). Since then, many other justification logic/modal logic pairs have been investigated, and justification logic has become a subject of independent interest, going beyond the original connection with intuitionistic logic. It is now known that there are infinitely many justification logics, but the exact extent of the family is not known. Justification logics are connected with their corresponding modal logics via Realization Theorems. A Realization Theorem connecting LP and S4 has a constructive proof, but there are other cases for which realization holds, but it is not known if a constructive proof exists. More recently, a first order version of LP has been developed, but I will not talk about it in detail. I will present a sketch of the basic propositional ideas.