# Blog Archives

These are the items posted in this seminar, currently ordered by their post-date, rather than by the event date. We will create improved views in the future. In the meantime, please click on the Seminar menu item above to find the page associated with this seminar, which does have a more useful view order.# Resource Sharing Linear Logic, I

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.

# Sub-Kripkean epistemic models I

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.

# Generic logical semantics of justifications III

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.

# Generic logical semantics of justifications II

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.

# Generic logical semantics of justifications.

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.

# Cut Elimination

Gentzen proved a famous cut elimination theorem using constructive methods. It is also possible to prove it non-constructively, with a conceptually simpler argument, but a constructive proof is important for a number of reasons. I will present the constructive argument for cut elimination, for classical propositional logic, formulated using tableaus. This is purely expository; there is nothing new. But it is a proof that every logician, or logician-to-be, should know, and I will cover the basics using a detailed set of slides which will be made available afterward, on my web site.

# Kripke completeness of strictly positive modal logics and related problems

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.

# The unreasonable effectiveness of Nonstandard Analysis.

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.

# Epistemic Updates on Algebras

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

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

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)

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

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

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

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.

# Towards Paraconsistent Game Theory

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.

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

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

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

# How (Not) To Aggregate Normative Reasons

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.

# Paraconsistent logic, evidence, and justification

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.