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.

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

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.

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.

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.

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.

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.

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.

Link to paper on arXiv:
http://arxiv.org/abs/1503.00362

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.

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.

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.

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.