Relating Semantics for Epistemic Logic

The aim of this paper is to explore the advantages deriving from the application of relating semantics in epistemic logic. As a first step, I will discuss two versions of relating semantics and how they can be differently exploited for studying modal and epistemic operators. Next, I consider several standard frameworks which are suitable for modelling knowledge and related notions, in both their implicit and their explicit form and present a simple strategy by virtue of which they can be associated with intuitive systems of relating logic. As a final step, I will focus on the logic of knowledge based on justification logic and show how relating semantics helps us to provide an elegant solution to some problems related to the standard interpretation of the explicit epistemic operators.

Structured argumentation dynamics

This paper develops a logical theory that unifies all three standard types of argumentative attack in AI, namely rebutting, undercutting and undermining attacks. We build on default justification logic that already represents undercutting and rebutting attacks, and we add undermining attacks. Intuitively, undermining does not target default inference, as undercutting, or default conclusion, as rebutting, but rather attacks an argument’s premise as a starting point for default reasoning. In default justification logic, reasoning starts from a set of premises, which is then extended by conclusions that hold by default. We argue that modeling undermining defeaters in the view of default theories requires changing the set of premises upon receiving new information. To model changes to premises, we give a dynamic aspect to default justification logic by using the techniques from the logic of belief revision. More specifically, undermining is modeled with belief revision operations that include contracting a set of premises, that is, removing some information from it. The novel combination of default reasoning and belief revision in justification logic enriches both approaches to reasoning under uncertainty. By the end of the paper, we show some important aspects of defeasible argumentation in which our logic compares favorably to structured argumentation frameworks.

A Conflict Tolerant Logic of Explicit Evidence

Standard epistemic modal logic is unable to adequately deal with the FrauchigerRenner paradox in quantum physics. We introduce a novel justification logic CTJ, in which the paradox can be formalized without leading to an inconsistency. Still CTJ is strong enough to model traditional epistemic reasoning. Our logic tolerates two different pieces of evidence such that one piece justifies a proposition and the other piece justifies the negation of that proposition. However, our logic disallows one piece of evidence to justify both a proposition and its negation. We present syntax and semantics for CTJ and discuss its basic properties. Then we give an example of epistemic reasoning in CTJ that illustrates how the different principles of CTJ interact. We continue with the formalization of the Frauchiger–Renner thought experiment and discuss it in detail. Further, we add a trust axiom to CTJ and again discuss epistemic reasoning and the paradox in this extended setting.

Semirings of Evidence

In traditional justification logic, evidence terms have the syntactic form of polynomials, but they are not equipped with the corresponding algebraic structure. We present a novel semantic approach to justification logic that models evidence by a semiring. Hence justification terms can be interpreted as polynomial functions on that semiring. This provides an adequate semantics for evidence terms and clarifies the role of variables in justification logic. Moreover, the algebraic structure makes it possible to compute with evidence. Depending on the chosen semiring this can be used to model trust, probabilities, cost, etc. Last but not least the semiring approach seems promising for obtaining a realization procedure for modal fixed point logics.

A logic of defeasible argumentation: Constructing arguments in justification logic

In the 1980s, Pollock’s work on default reasons started the quest in the AI community for a formal system of defeasible argumentation. The main goal of this paper is to provide a logic of structured defeasible arguments using the language of justification logic. In this logic, we introduce defeasible justification assertions of the type t : F that read as “t is a defeasible reason that justifies F”. Such formulas are then interpreted as arguments and their acceptance semantics is given in analogy to Dung’s abstract argumentation framework semantics. We show that a large subclass of Dung’s frameworks that we call “warranted” frameworks is a special case of our logic in the sense that (1) Dung’s frameworks can be obtained from justification logic-based theories by focusing on a single aspect of attacks among justification logic arguments and (2) Dung’s warranted frameworks always have multiple justification logic instantiations called “realizations”. We first define a new justification logic that relies on operational semantics for default logic. One of the key features that is absent in standard justification logics is the possibility to weigh different epistemic reasons or pieces of evidence that might conflict with one another. To amend this, we develop a semantics for “defeaters”: conflicting reasons forming a basis to doubt the original conclusion or to believe an opposite statement. This enables us to formalize non-monotonic justifications that prompt extension revision already for normal default theories. Then we present our logic as a system for abstract argumentation with structured arguments. The format of conflicting reasons overlaps with the idea of attacks between arguments to the extent that it is possible to define all the standard notions of argumentation framework extensions. Using the definitions of extensions, we establish formal correspondence between Dung’s original argumentation semantics and our operational semantics for default theories. One of the results shows that the notorious attack cycles from abstract argumentation cannot always be realized as justification logic default theories.

On sharp and single-conclusion justification models

Justification awareness models (JAMs) were proposed by S. Artemov as a tool for modelling epistemic scenarios such as Russell’s prime minister example. It was demonstrated that the sharpness and the single-conclusion property of a model play an essential role in the epistemic usage of JAMs. The problem to axiomatize these properties using the propositional justification language was left opened. We propose the solution and define a decidable justification logic $\textsf{J}_{\textit{ref}}$ that is sound and complete with respect to the class of all sharp single-conclusion justification models. We also provide the complete axiomatizations for the classes of all single-conclusion justification models and all sharp justification models.

Explicit analyses of proof/refutation interaction for constructible falsity and Heyting–Brouwer logic

Nelson’s logic of constructible falsity $\textsf{N}$ and Rauszer’s Heyting–Brouwer logic $\textsf{HB}$ are well-known cases of extensions of intuitionistic logic $\textsf{Int}$ enriched with novel connectives. Wansing has suggested that Gödel’s provability interpretation of $\textsf{Int}$ can be extended to these systems by pairing the category of formal proofs with a distinct category of formal refutations. In this paper, we extend the framework of Artemov’s justification logic to provide explicit analyses of $\textsf{N}$ and $\textsf{HB}$ (and the dual-intuitionistic logic $\textsf{DualInt}$) that respect a distinction between proofs and refutations. The application distinguishes the categories by reinterpreting the agents of multiple-agent justification logic as devices that operate exclusively on one or the other category. The analyses reveal that differences between $\textsf{N}$ and $\textsf{HB}$ can be reduced to competing interaction principles characterizing the coordination between proofs and refutations. We conclude by reappraising some of the unusual features of $\textsf{HB}$ in light of the explicit analysis of $\textsf{HB}$.

Natural deduction and semantic models of justification logic in the proof assistant Coq

The purpose of this paper is to present a formalization of the language, semantics and axiomatization of justification logic in Coq. We present proofs in a natural deduction style derived from the axiomatic approach of justification logic. Additionally, we present possible world semantics in Coq based on Fitting models to formalize the semantic satisfaction of formulas. As an important result, with this implementation, it is possible to give a proof of soundness for $\mathsf{L}\mathsf{P}$ with respect to Fitting models.