Justification logic began with Sergei Artemov’s work on an arithmetic semantics for intuitionistic logic, which made use of modal S4 and the Gödel embedding. Roughly speaking, a modal formula records that various subformulas are necessary, while a justification logic counterpart for the modal logic replaces modal operators with structured terms that track why these subformulas are necessary. Artemov’s work provided justification counterparts for S4 and its familiar sublogics. Since then, very many modal logics have turned out to possess justification counterparts. In fact, the family of modal logics with justification counterparts is infinite. Recently this phenomenon has been extended to some well-known non-canonical modal logics. I will present the basic ideas of an exploration that is still continuing, and not yet well understood.
Doxastic agency is about agentive control over beliefs. A flip-side of this are beliefs concerning the things an agent controls. This is the realm of practical knowledge and knowing-how. I will show how to analyze practical knowledge and knowing-how in epistemic stit logic. Time permitting, I will discuss if the same formal machinery can also be used to analyze and model doxastic agency.
JA-STIT, the stit logic of justification announcements, features a combination of stit logic with justification epistemic logic which is further extended with a machinery for public announcements of justifications. We present this logic against the backdrop of related systems combining stit and justifications. We look into expressivity of JA-STIT using a selection of examples and formal results. In terms of the latter, we focus on completeness and frame definability. Time permitting, we will also briefly consider the relationship of JA-STIT to the logics it extends, such as stit logic and justification logic.
Attribution of individual responsibility in cases of multi-agent interaction crucially depends on what each agent knows about the effect of her own actions. Reasoning about this is not trivial, since the effects of j's actions can vary depending on what other agents do. Thus, we need to reason on how the actions of other agents may change not only the world (as the totality of non-epistemic facts), but also the knowledge of any agent j. In this paper, we propose a dynamic-epistemic framework that meets this need. In particular, the frame-work includes a static part that details what each agent knows before any interaction is on, while the dynamic part details how the observation of the actions performed by other agents change j's knowledge of the effect of her own actions. I show that this framework captures a major legal standard for responsibility, which involves knowledge that one's own action is sufficient to cause a bad outcome, as well as the notions of inus condition introduced by Mackie (The Cement of the Universe, OUP, 1974) and inns condition introduced by Belnap (A Theory of Causation, BJPS, 56/2, 2005). This in turn helps to interpret the legal standard in light of a rigorous notion of “causing”.
We introduce a new semantics for a logic of explicit and implicit beliefs based on the concept of multi-agent belief base. Differently from existing Kripke-style semantics for epistemic logic in which the notions of possible world and doxastic/epistemic alternative are primitive, in our semantics they are non-primitive but are defined from the concept of belief base. We provide a complete axiomatization as well as a decidability result for our logic.
I present a possible worlds semantics for a hyperintensional belief revision operator, which reduces the logical idealization of cognitive agents affecting similar operators in doxastic and epistemic logics, as well as in standard AGM belief revision theory. (Revised) belief states are not closed under classical logical consequence; revising by inconsistent information does not perforce lead to trivialization; and revision can be subject to framing effects: logically or necessarily equivalent contents can lead to different revisions. Such results are obtained without resorting to non-classical logics, or to non-normal or impossible worlds semantics. The framework combines, instead, a standard semantics for propositional S5 with a simple mereology of topics.
Kripke models are widely used to specify epistemic situations: easy-to-desrcibe, often finite, Kripke models define truth values of all epistemic sentences. However, in this role, Kripke models and similar structures tacitly rely on an assumption of common knowledge of the model which manifests itself in the “Fully Explanatory Property”, FEP: a proposition true at all possible states is known at the reference state. Without (common) knowledge of the model, FEP is not valid, e.g., a proposition X can hold at all possible states unbeknown to the agent and no knowledge of X occurs.
There are conceptual problems with epistemic specifications via a Kripke model:
Our goal is to develop epistemic models free of the aforementioned limitations. As the first step, we maintain the view of a basic epistemic model M as a collection of possible states/worlds with given truth values of formulas at each state. Such an M with the induced Kripkean accessibility relations “what is known at the reference state holds at all accessible states” is not, generally speaking, a Kripke model because of the lack of FEP. It is easy to notice, however, that each basic epistemic model M is embedded into an appropriate Kripke model S (which we call “scaffolding model”) and viewed, informally, as the “observable fragment” of S. A scaffolding Kripke model S can be used as a specification tool for M.
Another subject of modernization is an epistemic state. We address the partial specifications issue by viewing epistemic states not as maximal consistent sets of formulas but rather as theories, i.e., deductively closed sets of formulas, not necessarily complete, with an appropriate alignment of theories at different epistemic states.
We argue for conceptual and practical value of new models, specifically for representing partial knowledge, asymmetric knowledge, and awareness.
A sequent calculus methodology for systems of agency based on branching time frames is proposed, starting with a complete and cut-free system for multi-agent deliberative STIT.
I will discuss the problem of proving cut elimination syntactically for some modal calculi with labels where the rule of contraction is not implicit in the logical rules. I will show that a simple cut-elimination procedure à la Gentzen is available in a weakly complete calculus for the basic modal logic K. I will also discuss the prospects of extending the result to a version of the calculus which has been proved to be strongly complete by P. Minari.
Some have argued that if an agent a's imagining A leads to a also imagining B, then a believes B conditional on A. However, it is sometimes not clear whether this amounts to believing the subjunctive conditional “if A were the case, B would be the case” or to a conditional state “if a were to believe A, then a would believe B”. In the talk, I aim to explore the relation between imagination and conditional beliefs. I start out with some philosophical considerations, and then enrich Olkhovikov and Wansing's STIT-imagination logic with a conditional belief operator, whose truth-condition is given in terms of neighborhoods. The semantics will validate a formula representing the idea that if an agent a's imagining A leads to a also imagining B, then a believes B conditional on A. As this is work in progress, I conclude by presenting some technical and interpretatory issues concerning the semantics.
In this talk I will present the tableau calculus for stit imagination logic from G. Olkhovikov and H. Wansing: An axiom system and a tableau calculus for STIT imagination logic, JPL, 2017.
Past decades have witnessed a variety of research on logics with a sole primitive modality that is essentially a combination of another modality and boolean connectives. For instance, in non-contingency logic, a formula is non-contingent iff it is either necessarily true or necessarily false, whereas a formula is contingent iff it is possibly true and also possibly false; in the logic of essence and accident, a formula is essential iff. once it is true, it is necessarily true, while a formula is accident iff. it is true but possibly false; in the logic of ignorance, a formula is ignored iff. it is both not known to be true and not known to be false. Despite being definable with known modalities such as necessity, knowledge or belief, these modalities have philosophical interests in their own right, and deserve to be studied independently. Notions like contingency are related to Hintikka's treatment of question embedding verbs like “know”, “remember”. From the mathematical point of view, there are technical difficulties and novelties in completely axiomatizing them over various classes of frames.
In this talk, I will present a pedagogical software to teach dynamic epistemic logic, called Hintikka's world. The tool is available here. The software presents Kripke worlds in thought baloons. I will also show to create new examples. The second part of the talk will be more technical: I will make an overview about algorithms for model checking, SAT and epistemic planning.