TR-2007025: Public Communication in Justification Logic
Bryan Renne · CUNY Academic Works (City University of New York) · 2007
Justification Logic is the study of a family of logics used to reason about justified true belief.Dynamic Epistemic Logic is the study of a family of logics obtained by adding various kinds of communication to the language of multi-modal logic, yielding languages for reasoning about communication and true belief.This paper is a first-step in merging these two areas, in that it brings the most basic kind of communication studied in Dynamic Epistemic Logic-the public announcement-over to Justification Logic.This gives us a language for reasoning about public announcements and justified true belief.After giving an overview of Justification Logic, the paper introduces a notion of bisimulation for Justification Logic.Bisimulation allows us to study the affect on language expressivity when we add various kinds of communication to the language.Among a number of expressivity results, we show that adding public announcements to the language of Justification Logic strictly increases language expressivity.This stands in contrast to the Plaza-Gerbrandy Theorem, which states that adding public announcements to multi-modal logic does not increase language expressivity.This leads us to extend the language of Justification Logic in order to provide a Plaza-Gerbrandy analog of multi-modal logic that we can use to reason about justified true belief.true in all of those states of affairs that look the same to me as the actual state of affairs [16].And to say that the Hintikka-belief of p is true (as in correct) means that p is in fact true in the actual state of affairs.So I Kripke-know something exactly when I Hintikka-believe that something and I am correct in this belief.Now if a formal language has a possible worlds semantics that makes true Hintikkabelief expressible in the language, then this language can be used to reason about Kripkeknowledge.The language of modal logic is an example: if K is a modal and ϕ is a formula, then the modal formula Kϕ-read it as "ϕ is known"-expresses the true Hintikka-belief of ϕ when we interpret this language via Kripke's semantics.Since Kripke's semantics for modal logic gives us a formal meaning for true belief, we are quite close to a formalization of Plato's definition of knowledge: knowledge is justified true belief.But while our interpretation of modal logic allows us to formalize the last two components of Plato's three-part definition, it falls short when we wish to formalize the first component, justification.Let us see why.Consider a formula of the form Kϕ ⊃ Kψ.Such a formula is a statement of conditional knowledge that says my knowledge of ψ follows from my knowledge of ϕ.But notice that while such a formula describes a connection between my knowledge of one thing and my knowledge of another, the formula fails to provide a reason as to why this connection holds, something we certainly want of our logical language if we are to say that this language incorporates a notion of justification.It is thus more accurate for us to read the formula Kϕ as "ϕ is known for some reason" because this formula merely asserts the existence of knowledge-it does not say why we have this knowledge.Justification Logic has recently been suggested as a means of remedying this shortcoming [5,6,4,12].The basic language of Justification Logic extends the language of propositional logic by introducing formula-labeling terms, allowing us to take a term t and a formula ϕ and form the new formula t : ϕ.Terms can be nested, so in the formula t : ϕ, the formula ϕ may itself contain terms.But the most important feature of terms is the fact that they have a certain derivation-compatible structure: for each derivation D of a theorem ϕ (in a later-defined system), we can construct a term t whose structure mimics that of D in such a way that t : ϕ is also a theorem.This allows us to think of the term t as a particular reason that explains why it is that ϕ is true.Justification Logic thus has a built-in notion of justification that, when combined with a possible worlds semantics [2, 13, 3], again allows us to capture true Hintikka-belief.Accordingly, we read t : ϕ as "ϕ is known for reason t."We then have a formalization of true belief in a logic with in-language justification, thereby capturing all three components of Plato's definition.So far Justification Logic has only been used to model static situations of knowledge (justified true belief).In this paper, we introduce public announcements into the language of Justification Logic.A public announcement is a kind of truthful public communication whose purpose is to create common knowledge among the hearers of the announcement.Public announcements are a basic concept in Dynamic Epistemic Logic, an area that studies communication and knowledge (true belief) by introducing various kinds of communication into the language of modal logic [23].Our paper is thus a first-step in merging the areas of 2 Justification Logic and Dynamic Epistemic Logic.Our task in this paper is to extend the language of Justification Logic so as to reason about public announcements alongside knowledge (justified true belief).After we introduce the syntax and semantics of of Justification Logic, we will define a notion of bisimulation for this language.Bisimulation allows us to study how language expressivity is affected when we introduce additional syntax to reason in the language about a given kind of communication such as public announcements.We will use our notion of bisimulation to show that adding public announcements to the language of Justification Logic strictly increases language expressivity, in contrast to the Plaza-Gerbrandy Theorem, which shows that adding public announcements to the language of modal logic does not increase language expressivity [18, 15].We will conclude by defining a natural extension for the language of Justification Logic.This extension has the property that adding public announcements does not increase language expressivity, and so this extension may be considered a Plaza-Gerbrandy analog of modal logic that we can use to reason about justified true belief. About Justification LogicJustification Logic refers to a family of logics that have a certain close relationship with LP, Artemov's Logic of Proofs [7].In this section we will define the syntax and semantics of LP and its multi-modal extensions. Syntax of Justification LogicDefinition 2.1 (LP P ).Let P be a set of propositional letters and let ⊥ be the propositional constant for falsity.Then the language of LP P is given by the following grammar.