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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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