Abstract
We propose a solution to the problem of logical omniscience in what we take to be its fundamental version: as concerning arbitrary agents and the knowledge attitude per se. Our logic of knowledge is a spin-off from a general theory of thick content, whereby the content of a sentence has two components: (i) an intension, taking care of truth conditions; and (ii) a topic, taking care of subject matter. We present a list of plausible logical validities and invalidities for the logic of knowledge per se for arbitrary agents, and isolate three explanatory factors for them: (1) the topic-sensitivity of content; (2) the fragmentation of knowledge states; (3) the defeasibility of knowledge acquisition. We then present a novel dynamic epistemic logic that yields precisely the desired validities and invalidities, for which we provide expressivity and completeness results. We contrast this with related systems and address possible objections.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Bergmann, M. (2006). Justification without awareness. Oxford: Clarendon Press.
Berto, F. (2018). Aboutness in imagination. Philosophical Studies, 175(8), 1871–1886.
Berto, F. (2019). Simple hyperintensional belief revision. Erkenntnis, 84(3), 559–575.
Berto, F., & Hawke, P. (2018). Knowability relative to information. Mind, Forthcoming.
Berto, F., & Jago, M. (2019). Impossible worlds. Oxford: Oxford University Press.
Bjerring, J.C. (2012). Impossible worlds and logical omniscience: an impossibility result. Synthese, 190, 2505–2024.
Bjerring, J.C., & Skipper, M. (2019). A dynamic solution to the problem of logical omniscience. Journal of Philosophical Logic, 48(3), 501–521.
Blackburn, P., de Rijke, M., Venema, Y. (2001). Modal logic, volume 53 of Cambridge tracts in theoretical computer science. Cambridge: Cambridge University Press.
Braddon-Mitchell, D., & Jackson, F. (2007). The philosophy of mind and cognition: an introduction, 2nd edn. Oxford: Blackwell Publishers.
Brown, J. (2018). Fallibilism: evidence and knowledge. Oxford: Oxford University Press.
Carnap, R. (1947). Meaning and necessity. Chicago University Press.
Christensen, D. (2004). Putting logic in its place: formal constraints on rational belief. Oxford: Oxford University Press.
Cresswell, M.J. (1985). Structured meanings: the semantics of propositional attitudes. Cambridge: MIT Press.
Crossley, J., & Humberstone, L. (1977). The logic of “actuality”. Reports on Mathematical Logic, 8, 11–29.
Dretske, F.I. (1970). Epistemic operators. Journal of Philosophy, 67(24), 1007–1023.
Dretske, F.I. (2005). The case against closure. In Steup, Sosa (Eds.) Contemporary debates in epistemology. 1st edn.: Wiley Blackwell, 13–26.
Fagin, R., & Halpern, J. (1988). Belief, awareness and limited reasoning. Artificial Intelligence, 34, 39–76.
Fagin, R., Halpern, J., Moses, Y., Vardi, M. (1995). Reasoning about knowledge. Cambridge: MIT Press.
Ferguson, T.M. (2014). A computational interpretation of conceptivism. Journal of Applied Non-Classical Logics, 24(4), 333–367.
Field, H. (1986). Critical notice: Stalnaker, Robert “Inquiry” Philosophy of Science, 53(3), 425–448.
Field, H. (1986). Stalnaker on intentionality: on Robert Stalnaker’s “Inquiry” Pacific Philosophical Quarterly, 67(2), 98–112.
Fine, K. (1986). Analytic implication. Notre Dame Journal of Formal Logic, 27, 169–79.
Fine, K. (2016). Angellic content. Journal of Philosophical Logic, 45(2), 199–226.
Floridi, L. (2015). Semantic conceptions of information. The Stanford Encyclopedia of Philosophy, http://plato.stanford.edu/entries/information-semantic/.
Gerbrandy, J., & Groeneveld, W. (1997). Reasoning about information change. Journal of Logic, Language and Information, 6(2), 147–169. ISSN 1572-9583.
Giordani, A. (2019). Axiomatizing the logic of imagination. Studia Logica, 107 (4), 639–657.
Harman, G. (1973). Thought. Princeton: Princeton University Press.
Harman, G. (1986). Change in view. Cambridge: MIT Press.
Hawke, P. (2016). Questions, topics and restricted closure. Philosophical Studies, 73(10), 2759–2784.
Hawke, P. (2018). Theories of Aboutness. Australasian Journal of Philosophy, 96(4), 697–723.
Hawthorne, J. (2004). Knowledge and lotteries. Oxford: Oxford University Press.
Hawthorne, J. (2005). The case for closureIn Steup, Sosa (Eds.) Contemporary debates in epistemology. 1st edn.: Wiley Blackwell, 26–43.
Hintikka, J. (1962). Knowledge and belief. An Introduction to the logic of the two notions. Ithaca: Cornell University Press.
Holliday, W. (2012). Knowing what follows: Epistemic closure and epistemic logic. PhD Dissertation, Stanford.
Holliday, W.H. (2015). Fallibilism and multiple paths to knowledge. In T. Gendler, & J. Hawthorne (Eds.) Oxford studies in epistemology, (Vol. 5 pp. 97–144): Oxford University Press.
Howe, M. (1970). Introduction to human memory. New York: Harper and Row.
Jago, M. (2007). Hintikka and Cresswell on logical omniscience. Logic and Logical Philosophy, 15, 325–54.
Jago, M. (2014). The impossible. An essay on hyperintensionality. Oxford: Oxford University Press.
Katzley, A. (1975). Human memory: Structures and processes. San Francisco: W.H Freeman.
Konolige, K. (1986). A deduction model of belief. San Mateo: Morgan Kaufman.
Lawlor, K. (2005). Living without closure. Grazer Philosophische Studien, 69 (1), 25–49.
Levesque, H. (1984). A logic of implicit and explicit belief. National conference on AI, AAAI-84, 198–202.
Levi, I. (1991). The fixation of belief and its undoing. Cambridge: Cambridge UP.
Lewis, D. (1982). Logic for equivocators. Nous, 16, 431–441.
Lewis, D. (1988). Relevant implication. Theoria, 54(3), 161–174.
Moore, R., & Hendrix, G. (1982). Computational models of belief and the semantics of belief claims. In P. S. Peters, & E. Saarinen (Eds.) Processes, beliefs and questions (pp. 107–127). Dordrecht: Reidel.
Parry, W.T. (1989). Analytic implication: its history, justification and varieties. In Norman, & Sylvan (Eds.) Directions in relevant logic (pp. 101–118): Kluwer Academic Publishers.
Partee, B.H. (1973). The semantics of belief-sentences. In Hintikka, K. J. J., Moravcsik, J. M. E., Suppes, P. (Eds.) Approaches to natural language: proceedings of the 1970 Stanford worskhop on grammar and semantics (pp. 309–336): D. Reidel Publishing Company.
Plaza, J. (1989). Logics of public communications. In Proceedings of the 4th international symposium on methodologies for intelligent systems. Reprinted as [50] (pp. 201–216).
Plaza, J. (2007). Logics of public communications. Synthese, 158(2), 165–179.
Priest, G. (2005). Towards non-being. The logic and metaphysics of intentionality. Oxford: Oxford University Press.
Priest, G. (2016). Thinking the impossible. Philosophical Studies, 173, 2649–2662.
Rantala, V. (1982). Impossible world semantics and logical omniscience. Acta Philosophica Fennica, 35, 106–115.
Ryle, G. (1933). About. Analysis, 1(1), 10–12.
Schipper, B. (2015). Awareness. In H. van Ditmarsch, J. Halpern, W. van der Hoek, B. Kooi (Eds.) Handbook of epistemic logic (pp. 79–146). London: College Publications.
Sedlar, I. (2015). Substructural epistemic logics. Journal of Applied Non-Classical Logics, 25, 256–285.
Stalnaker, R. (1984). Inquiry. Cambridge: MIT Press.
Stalnaker, R. (1991). The problem of logical omniscience, i. Synthese, 89(3), 425–440.
Titelbaum, M. (2014). Quitting certainties: a Bayesian framework modeling degrees of belief. Oxford: Oxford University Press.
van Benthem, J.F.A.K. (2011). Logical dynamics of information and interaction. Cambridge: Cambridge University Press.
van Benthem, J.F.A.K., & Velázquez-Quesada, F. (2009). Inference, promotion, and the dynamics of awareness. Knowledge, Rationality and Action, 177, 5–27.
van Ditmarsch, H., van der Hoek, W., Kooi, B. (2008). Dynamic epistemic logic. Dordrecht: Springer.
Wansing, H. (1990). A general possible worlds framework for reasoning about knowledge and belief. Studia Logica, 49, 523–39.
Williamson, T. (2000). Knowledge and its limits. Oxford: Oxford University Press.
Yablo, S. (2014). Aboutness. Princeton: Princeton University Press.
Yalcin, S. (2018). Belief as question-sensitive. Philosophy and Phenomenological Research, 97(1), 23–47.
Acknowledgments
Many thanks to our anonymous referees for astute and constructive comments. Special thanks to Alexandru Baltag for stimulating feedback that significantly influenced the contents of Section ??. Versions of the present work were presented at the following conferences and workshops: the fourth meeting of the ‘From Shared Evidence to Group Attitudes’ project, University of Bayreuth, April 18-19, 2018; ‘Reasoning in Social Contexts’ at the Royal Netherlands Academy of Arts and Sciences, Amsterdam, May 31-June 2, 2018; ‘Models of Bounded Reasoning in Individuals and Groups’ at the Lorentz Center, Leiden, July 2-6, 2018; the Super-Special seminar slot at Arché, University of St Andrews, November 29, 2018; and the ‘Workshop on the Occasion of Johan van Benthem’s 70th birthday’ in Amsterdam, June 12, 2019. We thank these audiences for their helpful questions and remarks. This research is published within the project ‘The Logic of Conceivability’, funded by the European Research Council (ERC CoG), Grant Number 681404.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Appendices
Appendix A: Proof of Theorem 2
We call a sentence ψ of \(\mathcal {EL}\)Boolean if it does not include occurrences of \(i, \Box , K_{i},\) or [i : φ]. The following auxiliary lemma will be useful in the proof of Theorem 2:
Lemma 4
For all epistemic update models\({\mathcal{M}}=\langle W, @, \mathbb {T}, \oplus , \mu , v, t \rangle \), all\(\varphi \in \mathcal {EL}\), \(i\in \mathcal {F}\), and all Boolean sentencesψ, we have\(|\psi |_{{\mathcal{M}}}=|\psi |_{{\mathcal{M}}^{i}_{\varphi }}\).
Proof
Follows via an easy induction on the structure of ψ. □
Proof of Theorem 2:
- Invalidities: :
-
In figures of counterexamples, white nodes represent possible worlds, black nodes represent possible topics. Valuation and topic assignment are given by labelling each node with atomic formulae. We omit labelling when a node is assigned every element in \(\mathcal {A}\mathcal {T}\).
Counterexample for (9)–(11) and (15)–(16): These schemas are invalid due to topicality. Without loss of generality (w.l.o.g.), let \(\mathcal {F}=\{i\}\) and consider the model \({\mathcal{M}}_{1}=\langle W, @, \mathbb {T}, \oplus , \mu , v, t \rangle \) such that W = {@}, \(\mathbb {T}=\{a, b, c\}\) with b≠c, b < a, and c < a, v(i) = v(p) = v(q) = {@}, and t(p) = t(i) = b and t(q) = c (Fig. 3). (We do not need to specify μ since it is irrelevant for these schemas.) Then, (9) is invalid since \({\mathcal{M}}_{1}, @\not \vDash \Box (p\supset q)\supset (Kp\supset Kq)\): \({\mathcal{M}}_{1}, @\vDash \Box (p\supset q)\) (since |p| = |q|) and \({\mathcal{M}}_{1}, @\vDash K_{i} p\) (since v(i) = |p| and t(p) ≤ t(i)). However, \({\mathcal{M}}_{1}, @\not \vDash K_{i} q\) since t(q)≦̸t(i). As \(\mathcal {F}=\{i\}\), we obtain that \({\mathcal{M}}_{1}, @\not \vDash \Box (p\supset q) \supset (Kp\supset Kq)\). Similarly, (10) is invalid since \({\mathcal{M}}_{1}, @\not \vDash \Box q\supset K q\), and (11) is invalid since (q ∨¬q) is valid but \({\mathcal{M}}_{1}, @\not \vDash K(q\vee \neg q)\) for t(q)≦̸t(i). Moreover, (15) and (16) are invalid since \({\mathcal{M}}_{1}, @ \not \vDash K\neg \neg p\supset K\neg (\neg p\wedge q)\) and \({\mathcal{M}}_{1}, @ \not \vDash Kp\supset K\neg (\neg p\wedge q)\), respectively: it is easy to verify that \({\mathcal{M}}_{1}, @ \vDash K\neg \neg p\) and \({\mathcal{M}}_{1}, @ \vDash K p\), but \({\mathcal{M}}_{1}, @\not \vDash K\neg (\neg p\wedge q)\) as t(¬(¬p ∧ q)) = t(p) ⊕ t(q) = a≦̸t(i).
Counterexample for (17)–(19): These schemas are invalid due to fragmentation. W.l.o.g., let \(\mathcal {F}=\{i, j\}\) and consider the model \({\mathcal{M}}_{2}=\langle W, @, \mathbb {T}, \oplus , \mu , v, t \rangle \) such that W = {@,w1,w2}, v(i) = {@,w1}, v(j) = v(p) = {@,w2}, and v(q) = {@}, \(\mathbb {T}=\{a\}\), and t(φ) = a for all \(\varphi \in \mathcal {EL}\). (Since every \(\varphi \in \mathcal {EL}\) is mapped to the same topic, the topicality constraints will be trivially satisfied.) Then, (17) is invalid since \({\mathcal{M}}_{2}, @\not \vDash K(p\supset q) \supset (Kp\supset Kq)\): \({\mathcal{M}}_{2}, @\vDash K_{i} (p\supset q)\) (since \(v(i)= |p\supset q|\)) and \({\mathcal{M}}_{2}, @\vDash K_{j} p\) (since v(j) = |p|), thus, \({\mathcal{M}}_{2}, @\vDash K (p\supset q) \) and \({\mathcal{M}}_{2}, @\vDash K p\). However, \({\mathcal{M}}_{2}, @\not \vDash Kq\) since \({\mathcal{M}}_{2}, @ \not \vDash K_{i} q\) and \({\mathcal{M}}_{2}, @ \not \vDash K_{j} q\) (as \(v(i)\not \subseteq |q|\) and \(v(j)\not \subseteq |q|\), respectively). For (18) and (19), consider \({\mathcal{M}}_{2}\) with μ(P,Q) = P ∩ Q for all \(P, Q\in \mathbb {I}_{@}\). Then, (18) is invalid since \({\mathcal{M}}_{2}, @\vDash \neg [j: p ][i: p\supset q] Kq\): \({\mathcal{M}}_{2}, @\vDash p\) and \(({\mathcal{M}}_{2})^{j}_{p}, @\vDash p\supset q\), but, \(({({\mathcal{M}}_{2})^{j}_{p})}^{i}_{p \supset q}, @\not \vDash K_{i} q \vee K_{j} q\) (since \({({v_{p}^{j}})}^{i}_{p\supset q}(j)= \{@, w_{2}\}\) and \({({v_{p}^{j}})}^{i}_{p\supset q}(i)= \{@, w_{1}\}\), and \(({({\mathcal{M}}_{2})^{j}_{p})}^{i}_{p \supset q}, w_{1}\not \vDash q\) and \(({({\mathcal{M}}_{2})^{j}_{p})}^{i}_{p \supset q}, w_{2}\not \!\vDash \! q\)). Similarly, (19) is invalid since \({\mathcal{M}}_{2}, @\!\vDash \! \neg [i{}:{} p\!\supset \! q][j{}:{} p ] Kq\).
Counterexample for (20) and (21): These schemas are invalid due to non-monotonicty of knowledge update. The counterexample \({\mathcal{M}}_{2}\) in Fig. 4 with \(\mu ^{\prime }(P, Q)\) = Q for all \(P, Q\in \mathbb {I}_{@}\) invalidates (20) and (21): \({\mathcal{M}}_{2}, @\vDash K_{i}(p\supset q)\wedge K_{j} p\), but \({\mathcal{M}}_{2}, @\not \vDash [i:j]Kq\) and \({\mathcal{M}}_{2}, @\not \vDash [j:i]Kq\). For \({\mathcal{M}}_{2}, @\not \vDash [i:j]Kq\), observe that \({v_{j}^{i}}(i)= {v_{j}^{i}}(j)= \{@, w_{2}\}\not \subseteq |q|\), thus, \(({\mathcal{M}}_{2})^{i}_{j}\not \vDash K_{i}q\vee K_{j} q\). For \({\mathcal{M}}_{2}, @\not \vDash [j:i]Kq\), observe that \({v_{i}^{j}}(i)= {v_{i}^{j}}(j)= \{@, w_{1}\}\not \subseteq |q|\), thus, \(({\mathcal{M}}_{2})^{j}_{i}\not \vDash K_{i}q\vee K_{j} q\).
Counterexample for (22)–(27): These principles are invalid due to non-monocity of knowledge update. It is easy to see that counterexamples invalidating (26) and (27) are also counterexamples for (24) and (25), respectively. Moreover, (24) and (25) are special cases of (22) and (23), respectively. Consider the model \({\mathcal{M}}_{3}=\langle W, @, \mathbb {T}, \oplus , \mu , v, t \rangle \) such that W = {@,w1}, \(\mathbb {T}=\{a\}\), v(i) = v(p) = {@} for all \(i\in \mathcal {F}\), and v(q) = W, t(φ) = a for all \(\varphi \in \mathcal {EL}\), and μ(P,Q) = Q for all \(P, Q\in \mathbb {I}_{@}\) (Fig. 5). As every frame of mind is mapped to the same set of possible wolds, we do not need to consider fragmentation. Similarly since every \(\varphi \in \mathcal {EL}\) is mapped to the same topic, the topicality constraints will be trivially satisfied. Then, (26) is invalid since \({\mathcal{M}}_{3}, @\not \vDash [i: p][i: q] K_{i} p\): \({\mathcal{M}}_{3}, @\vDash p\) and \(({\mathcal{M}}_{3})^{i}_{p}, @\vDash q\) but \({(({\mathcal{M}}_{3})^{i}_{p})}^{i}_{q}, @\not \vDash K_{i}p\) since \({({v_{p}^{i}})}_{q}^{i}(i)=W\) and \({(({\mathcal{M}}_{3})^{i}_{p})}^{i}_{q} , w_{1}\not \vDash p\). Similarly, (27) is invalid since \({\mathcal{M}}_{3}, @\not \vDash K_{i}p\supset [i: q]K_{i} p\): \({\mathcal{M}}_{3}, @ \vDash K_{i}p\) and \({\mathcal{M}}_{3}, @ \vDash q\), but \(({\mathcal{M}}_{3})^{i}_{q}, @\not \vDash K_{i}p\) since \({v_{q}^{i}}(i)=W\) and \(({\mathcal{M}}_{3})^{i}_{q}, w_{1}\not \vDash p\).
- Validities: :
-
Let \({\mathcal{M}} = \langle W,\! @,\! \mathbb {\!T}, \!\oplus ,\! \mu ,\! v,\! t \rangle \) be an epistemic update model and w ∈ W:
(12) \(\vDash \Box (\varphi \supset \psi )\supset (\Box \varphi \supset \Box \psi )\): Suppose \({\mathcal{M}}, w\vDash \Box (\varphi \supset \psi )\) and \({\mathcal{M}}, w\vDash \Box \varphi \). While the former means that \(|\varphi |\subseteq |\psi |\), the latter means |φ| = W. Therefore, |ψ| = W, i.e., \({\mathcal{M}}, w\vDash \Box \psi \).
(13) \(\vDash K(\varphi \wedge \psi )\supset K\varphi \): Suppose \({\mathcal{M}}, w\vDash K(\varphi \wedge \psi )\). This means, by the definition of K, that there is an \(i\in \mathcal {F}\) such that \({\mathcal{M}}, w\vDash K_{i}(\varphi \wedge \psi )\), i.e., that \(v(i)\subseteq |\varphi \wedge \psi |\) and t(φ ∧ ψ) ≤ t(i). Since \(v(i)\subseteq |\varphi \wedge \psi |\subseteq |\varphi |\) and t(φ) ≤ t(φ) ⊕ t(ψ) = t(φ ∧ ψ) ≤ t(i), we obtain \({\mathcal{M}}, w\vDash K_{i}\varphi \). Thus, \({\mathcal{M}}, w\vDash K\varphi \). The validity proofs of (14), and (30)–(32) follow similarly.
(28) ⊧ [p]Kp: Let \(i\in \mathcal {F}\) and suppose \({\mathcal{M}}, @\vDash p\). We then have that \({v^{i}_{p}}(i)=\mu (v(i), |p|)\subseteq |p|= |p|_{{\mathcal{M}}^{i}_{p}}\) (by Lemma 4). Moreover, \({t^{i}_{p}}(i)=t(i)\oplus t(p)\geq t(p)={t^{i}_{p}}(p)\). Therefore, \({\mathcal{M}}^{i}_{p}, w\vDash K_{i}p\), implying that \({\mathcal{M}}^{i}_{p}, w\vDash Kp\). Thus, \({\mathcal{M}}, w\vDash [i: p] Kp\). Since i has been chosen arbitrarily from \(\mathcal {F}\), we obtain that \({\mathcal{M}}, w\vDash [p] Kp\).
(29) \(\vDash Kp\supset [q]\neg K\neg p\): Suppose \({\mathcal{M}}, w\vDash Kp\) and let \(i\in \mathcal {F}\) such that \({\mathcal{M}}, @\vDash q\). The former implies that \({\mathcal{M}}, w\vDash K_{j}p\) for some \(j\in \mathcal {F}\). In particular, since @ ∈ v(k) for all \(k\in \mathcal {F}\), we have \({\mathcal{M}}, @\vDash p\). Then, by Lemma 4, we obtain that \({\mathcal{M}}^{i}_{q}, @ \vDash p\). By the definition of μ, we also have that \(@\in {v^{i}_{q}}(k)\) for all \(k\in \mathcal {F}\). Therefore, \({\mathcal{M}}^{i}_{q}, w\vDash \neg K_{k}\neg p\) for all \(k\in \mathcal {F}\), meaning that \({\mathcal{M}}^{i}_{q}, w\vDash \neg K\neg p\). Hence, \({\mathcal{M}}, w\vDash [i:q]\neg K\neg p\). Since i has been chosen arbitrarily from \(\mathcal {F}\), we obtain that \({\mathcal{M}}, w\vDash [q]\neg K\neg p\), thus, \({\mathcal{M}}, w\vDash Kp \supset [q]\neg K\neg p\). □
Appendix B: Soundness and Completeness for \(\mathcal {EL}^{+}_{-}\), \(\mathcal {EL}^{*}_{-}\), and \(\mathcal {EL}^{*}\)
We provide soundness and completeness results for \(\mathcal {EL}^{+}_{-}\), \(\mathcal {EL}^{*}_{-}\), and \(\mathcal {EL}^{*}\). The following syntactic abbreviations will matter: for any \(\varphi \in \mathcal {EL}^{*}\), \(\mathcal {A}\mathcal {T}(\varphi )\) denotes the set of atomic formulae occurring in φ and we will use ‘\(\overline {\varphi }\)’ to denote the tautology \(\bigwedge _{x\in \mathcal {A}\mathcal {T}(\varphi })(x\vee \neg x)\), following a similar idea in [26].
All our soundness and completeness results are proven with respect to the class of epistemic update models whose topic assignment function is defined in the following way:
-
\(t: \mathcal {A}\mathcal {T} \to \mathbb {T}\) is a topic function assigning a topic to each element in \(\mathcal {A}\mathcal {T}\). t extends to the whole \(\mathcal {EL}^{*}\) by taking the topic of a sentence φ as the fusion of the elements in \(\mathcal {A}\mathcal {T}(\varphi )\):
$$ t(\varphi)=\oplus \mathcal{A}\mathcal{T}(\varphi)= t(x_{1})\oplus {\dots} \oplus t(x_{k}) $$where \(\mathcal {A}\mathcal {T}(\varphi )=\{x_{1}, \dots , x_{k}\}\).
≤ again denotes topic inclusion as defined in Section 4.1. The topic of a complex sentence φ, defined from its primitive components in \(\mathcal {A}\mathcal {T}(\varphi )\), makes all the logical connectives and modal operators in \(\mathcal {EL}^{*}\) topic-transparent, that is,
-
\(t(\Box \varphi ) = t(A\varphi ) = t(\neg \varphi ) = t(\varphi ) \)
-
\(t(K_{\psi }\varphi ) = t(\varphi \wedge \psi ) = t(\varphi \vee \psi ) =t(\varphi \supset \psi ) =t(\varphi \equiv \psi )= t(\varphi )\oplus t(\psi )\)
-
t([i : φ]ψ) = (t(i) ⊕ t(φ)) ⊕ t(ψ)
Topic-transparency of the truth-functional connectives has already been argued for in Section 1 and formally captured in Definition 1. The only further constraint we impose here is the topic-transparency of the modal operators Kψφ, \(\Box \varphi \), Aφ, and [i : φ]ψ. This is admittedly an idealization, but for technical purposes, in this paper we can live with this idealization, as Theorem 2 still holds with respect to epistemic update models with the above constraint. In the remainder of this appendix, all models are implicitly assumed to obey this constraint on t.
We first provide a sound and complete axiomatization for \(\mathcal {EL}^{*}_{-}\) (Appendix B.1). The completeness result for \(\mathcal {EL}^{+}_{-}\) follows similarly, so we omit many details and only point out the differences (Appendix B.1.1). The completeness for \(\mathcal {EL}^{*}\) will follow from the completeness of \(\mathcal {EL}^{*}_{-}\) via a set of sound reduction axioms (Appendix B.2).
2.1 B.1 The (static) Logic of Knowledge Over \(\mathcal {EL}^{*}_{-}\)
Since \(\mathcal {EL}^{*}_{-}\) does not have the dynamic operator, the update function μ does not play any role in its interpretation in epistemic update models. We therefore opt for simplicity and interpret \(\mathcal {EL}^{*}_{-}\) in what we call epistemic models, \({\mathcal{M}}=\langle W, @, \mathbb {T}, \oplus , v, t \rangle \), obtained by removing μ from epistemic update models.
To recap, given an epistemic model \({\mathcal{M}}=\langle W, @, \mathbb {T}, \oplus , v, t \rangle \) and w ∈ W, we define the satisfaction relation\(\vDash \) for the atomic formulae, Booleans, and \(\Box \varphi \) as in Definition 2; for Kψφ and Aφ we have:
Truth in a model and validity are defined as before (see Section 4.1). Soundness and completeness are defined in a standard way with respect to the global notion of validity denoted by \(\vDash \).
Lemma 5
Let\(\langle W, @, \mathbb {T}, \oplus , v, t \rangle \)be an epistemic model. Then, for any\(\varphi \in \mathcal {EL}^{*}_{-}\), w ∈ W, and update functionμ (as described in Definition 1), we have
Proof
Follows via an easy induction on the structure of φ as μ does not play any role in the interpretation of the sentences in \( \mathcal {EL}^{*}_{-}\). □
Observation 6
-
(1)
For all \(\varphi \in \mathcal {EL}_{-}^{*}\), \(\vDash \overline {\varphi }\).
-
(2)
\(\vDash K_{\varphi }\psi \equiv (K_{\varphi }\overline {\psi } \wedge \Box (\varphi \supset \psi ))\).Footnote 1
Table 1 presents a sound and complete axiomatization EL∗ of epistemic logic over \(\mathcal {EL}_{-}^{*}\). The notion of derivation, denoted by \(\vdash _{\mathsf {EL}^{*}}\), in EL∗ is defined as usual. Thus, \(\vdash _{\mathsf {EL}^{*}}\varphi \) means φ is a theorem of EL∗. For any set of formulas \({\Gamma }\subseteq \mathcal {EL}_{-}^{*}\) and any \(\varphi \in \mathcal {EL}_{-}^{*}\), we write \({\Gamma } \vdash _{\mathsf {EL}^{*}} \varphi \) if there exists finitely many formulas \(\varphi _{1}, \dots , \varphi _{n}\in {\Gamma }\) such that \(\vdash _{\mathsf {EL}^{*}}(\varphi _{1}\wedge {\dots } \wedge \varphi _{n})\supset \varphi \).
Theorem 7
The following are derivable fromEL∗:
-
(1)
from\(\vdash _{\mathsf {EL}^{*}} \varphi \equiv \psi , \vdash _{\mathsf {EL}^{*}} K_{\varphi }\overline {\psi }, and \vdash _{\mathsf {EL}^{*}} K_{\psi }\overline {\varphi }\), infer\(\vdash _{\mathsf {EL}^{*}} K_{\chi } \varphi \equiv K_{\chi } \psi \)and\(\vdash _{\mathsf {EL}^{*}}K_{\varphi }\chi \equiv K_{\psi }\chi \),
-
(2)
(NecA) from\(\vdash _{\mathsf {EL}^{*}}\varphi \)infer\(\vdash _{\mathsf {EL}^{*}}A\varphi \),
-
(3)
\(\vdash _{\mathsf {EL}^{*}}A(\varphi \wedge \psi ) \equiv A\varphi \wedge A\psi \),
Proof
(1) follows from Ax4, Ax6, and \(\mathsf {S5}_{\Box }\). Item (2) follows from necessitation for \(\Box \) and Ax1, and (3) is derived from KA and (NecA) in a standard way.
□
Soundness of EL∗ is a matter of routine validity check, so we skip its proof. The rest of this section is devoted to the completeness proof of EL∗, which is presented in full detail.
We say that Γ is EL∗-consistent if \({\Gamma } \not \vdash _{\mathsf {EL}^{*}}\bot \), and EL∗-inconsistent otherwise. We omit the tag EL∗ and say (in)consistent when the logic is contextually clear. A sentence φ is consistent with Γ if Γ ∪{φ} is consistent (or, equivalently, if \({\Gamma }\not \vdash _{\mathsf {EL}^{*}}\neg \varphi \)). Finally, a set of formulas Γ is a maximally consistent set (or, in short, mcs) if it is consistent and any set of formulas properly containing Γ is inconsistent [8]. Footnote 2
Lemma 8
For every mcs Γ ofEL∗and\(\varphi , \psi \in \mathcal {EL}_{-}^{*}\), the following hold:
-
(1)
\({\Gamma }\vdash _{\mathsf {EL}^{*}} \varphi \)iffφ ∈Γ,
-
(2)
if φ ∈Γ and\(\varphi \supset \psi \in {\Gamma }\), thenψ ∈Γ,
-
(3)
if\(\vdash _{\mathsf {EL}^{*}} \varphi \)thenφ ∈Γ,
-
(4)
φ ∈Γ andψ ∈Γ iffφ ∧ ψ ∈Γ,
-
(5)
φ ∈Γ iff ¬φ∉Γ.
Proof
Standard. □
Lemma 9 (Lindenbaum’s Lemma)
EveryEL∗-consistent set can be extended to a maximally consistent one.
Proof
Standard. □
Let \(\mathcal {X}\) be the set of all maximally consistent sets of EL∗. Define \(\sim _{\Box }\) on \(\mathcal {X}\) as
It is standard to prove that \(\sim _{\Box }\) is an equivalence relation, as \(\Box \) is an S5 operator. To define the canonical model, we need some auxiliary definitions and lemmas.
Lemma 10
For all\({\Gamma }\in \mathcal {X}\), \(@_{\Gamma } =\{\varphi \in \mathcal {EL}_{-}^{*} : A\varphi \in {\Gamma }\}\)is a maximally consistent set such that\({\Gamma } \sim _{\Box } @_{\Gamma }\)and\(1\wedge \dots \wedge n\in @_{\Gamma }\).
Proof
Suppose that \(@_{\Gamma } =\{\varphi \in \mathcal {EL}_{-}^{*} : A\varphi \in {\Gamma }\}\) is not consistent. This means that there are finitely many \(\varphi _{1}, \dots , \varphi _{k}\in @_{\Gamma } \) such that \(\vdash _{\mathsf {EL}^*} (\varphi _1\wedge {\dots } \wedge \varphi _k)\supset \bot \). This implies, in particular, that \(\vdash _{\mathsf {EL}^*} (\varphi _1\wedge {\dots } \wedge \varphi _{k-1})\supset \neg \varphi _k\). Then, by KA, Theorem 7.(2) and 7.(3), we have \(\vdash _{\mathsf {EL}^{*}}(A\varphi _{1} \wedge {\dots } \wedge A\varphi _{k-1})\supset A\neg \varphi _{k}\). As \(A\varphi _{1}, \dots , A\varphi _{k-1}\in {\Gamma }\), we have A¬φk ∈Γ. This means, by DuaA, that ¬Aφk ∈Γ, contradicting consistency of Γ. Therefore, @Γ is consistent. Now suppose that @Γ is not maximal. This means that there is a \(\psi \in \mathcal {EL}_{-}^{*}\) such that ψ∉@Γ and @Γ ∪{ψ} is consistent. But, as ψ∉@Γ, we have Aψ∉Γ, thus, by Lemma 8.(5) and DuaA, A¬ψ ∈Γ. This means that ¬ψ ∈ @Γ, which makes @Γ ∪{ψ} inconsistent. Therefore, @Γ is maximal too. By Ax3 and Lemma 8.(3), we have \(A(1\wedge {\dots } \wedge n)\in {\Gamma }\), therefore, \(1\wedge {\dots } \wedge n\in @_{\Gamma }\). Now take an arbitrary \(\varphi \in \mathcal {EL}_{-}^{*}\) and suppose that \(\Box \varphi \in {\Gamma }\). Then, by Ax1 and Lemmas 8.(2) and 8.(3), Aφ ∈Γ. This means that φ ∈ @Γ. Therefore, we also obtain that \({\Gamma } \sim _{\Box } @_{\Gamma }\). □
For \({\Gamma } \in \mathcal {X}\), let \(\approx _{\Gamma }\subseteq \mathcal {EL}_{-}^{*} \times \mathcal {EL}_{-}^{*}\) such that
In the following proofs, we make repeated use of Lemma 8 in a standard way as in the proof of Lemma 10 and omit mention of it.
Lemma 11
For all\({\Gamma } \in \mathcal {X}\), ≈Γis an equivalence relation. Moreover, for all\({\Gamma }, {\Delta }\in \mathcal {X}\)such that\({\Gamma } \sim _{\Box } {\Delta }\), we have ≈Γ =≈Δ.
Proof
Let \({\Gamma } \in \mathcal {X}\) and \(\varphi , \psi , \chi \in \mathcal {EL}_{-}^{*}\).
-
reflexivity: By Ax8, we have \(\vdash _{\mathsf {EL}^{*}} K_{\varphi }\overline {\varphi }\), thus, φ ≈Γφ.
-
symmetry: Suppose φ ≈Γψ. This means, by the defn. of ≈Γ, that \(K_{\varphi }\overline {\psi }, K_{\psi }\overline {\varphi }\in {\Gamma }\). Therefore, \(K_{\psi }\overline {\varphi }, K_{\varphi }\overline {\psi }\in {\Gamma }\), i.e., ψ ≈Γφ.
-
transitivity: Suppose φ ≈Γψ and ψ ≈Γχ. This means that (a) \(K_{\psi }\overline {\varphi }\in {\Gamma }\), (b) \(K_{\varphi }\overline {\psi }\in {\Gamma }\), (c) \(K_{\psi }\overline {\chi }\in {\Gamma }\), and (d) \(K_{\chi }\overline {\psi }\in {\Gamma }\). Then, by Ax6, (b), and (c), \(K_{\varphi }\overline {\chi }\in {\Gamma }\). Similarly, by Ax6, (a), and (d), \(K_{\chi }\overline {\varphi }\in {\Gamma }\). Therefore, φ ≈Γχ.
For the last part, let \({\Gamma }, {\Delta }\in \mathcal {X}\) such that \({\Gamma } \sim _{\Box } {\Delta }\). Suppose φ ≈Γψ. This means that \(K_{\varphi }\overline {\psi }, K_{\psi }\overline {\varphi }\in {\Gamma }\). Then, by Ax5, we obtain that \(\Box K_{\varphi }\overline {\psi }, \Box K_{\psi }\overline {\varphi }\in {\Gamma }\). As \({\Gamma } \sim _{\Box } {\Delta }\), we conclude that \(K_{\varphi }\overline {\psi }, K_{\psi }\overline {\varphi }\in {\Delta }\), i.e., φ ≈Δψ. For the other direction, use the symmetry of \(\sim _{\Box }\). □
Let \([\varphi ]_{\Gamma }=\{ \psi \in \mathcal {EL}_{-}^{*} : \varphi \approx _{\Gamma } \psi \}\), i.e., [φ]Γ is the equivalence class of φ with respect to ≈Γ.
Definition 3 (Canonical Model for Γ0)
Let Γ0 be a mcs of EL∗. The canonical model for Γ0 is the tuple \({\mathcal{M}}^{c}= \langle W^{c}, @_{{\Gamma }_{0}}, \mathbb {T}^{c}, \oplus ^{c}, v^{c}, t^{c} \rangle \), where
-
\(W^{c}=\{\Gamma \in \mathcal {X} : {\Gamma }_{0}\sim _{\Box } {\Gamma }\}\),
-
\(@_{{\Gamma }_{0}}=\{\varphi \in \mathcal {EL}_{-}^{*} : A\varphi \in {\Gamma }_{0}\}\),
-
\(\mathbb {T}^{c}=\{[\varphi ]_{{\Gamma }_{0}} : \varphi \in \mathcal {EL}_{-}^{*}\}\) (we omit the subscript Γ0 when it is clear from the context),
-
\(\oplus ^{c}: \mathbb {T}^{c} \times \mathbb {T}^{c} \to \mathbb {T}^{c}\) such that \([\varphi ]\oplus ^{c} [\psi ]=[\varphi \wedge \psi ]\),
-
\(t^{c}: \mathcal {EL}_{-}^{*} \to \mathbb {T}^{c}\) such that, for all \(x\in \mathcal {A}\mathcal {T}\), tc(x) = [x] and \(t^{c}(\varphi )=\oplus ^{c}\mathcal {A}\mathcal {T}(\varphi )\),
-
\(v^{c}: \mathcal {A}\mathcal {T}\to \mathcal {P}(W^{c})\) such that \(v^{c}(x)=\{\Gamma \in W^{c} : x\in {\Gamma }\}\).
The topic inclusion relation ≤c on the canonical model is defined in the usual way.
Lemma 12
Given a mcs Γ0ofEL∗and the canonical model\({\mathcal{M}}^{c}= \langle W^{c}, @_{{\Gamma }_{0}}, \mathbb {T}^{c}, \oplus ^{c}, v^{c}, t^{c} \rangle \) for Γ0as described above, we have
-
(1)
\(@_{{\Gamma }_{0}}\in W^{c}\),
-
(2)
\(i\in @_{{\Gamma }_{0}}\)for all\(i\in \mathcal {F}\),
-
(3)
for all\(\varphi \in \mathcal {EL}_{-}^{*}\)and Γ ∈ Wc, if\(\varphi \in @_{{\Gamma }_{0}}\)thenAφ ∈Γ,
-
(4)
for all Γ ∈ Wc, \(@_{\Gamma }=@_{{\Gamma }_{0}}\).
Proof
-
(1)
By Lemma 10.
-
(2)
By Lemmas 10 and 8.(4).
-
(3)
Let \(\varphi \in \mathcal {EL}_{-}^{*}\) such that \(\varphi \in @_{{\Gamma }_{0}}\), i.e., Aφ ∈Γ0. Then, by Ax2, we have \(\Box A\varphi \in {\Gamma }_{0}\). Hence, by the definition of Wc, Aφ ∈Γ f or all \({\Gamma }\in W^{c}\).
-
(4)
\(@_{{\Gamma }_{0}}\subseteq @_{\Gamma }\) follows directly from item (3). For \(@_{\Gamma }\subseteq @_{{\Gamma }_{0}}\), suppose φ ∈ @Γ, i.e., that Aφ ∈Γ. Then, by Ax2, we have \(\Box A\varphi \in {\Gamma }\). As Γ ∈ Wc, i.e., \({\Gamma }\sim _{\Box } {\Gamma }_{0}\), we obtain that Aφ ∈Γ0, i.e., \(\varphi \in @_{{\Gamma }_{0}}\).
□
Lemma 13
The canonical model\({\mathcal{M}}^{c}= \langle W^{c}, @_{{\Gamma }_{0}}, \mathbb {T}^{c}, \oplus ^{c}, v^{c}, t^{c} \rangle \)is an epistemic model.
Proof
-
\(@_{{\Gamma }_{0}}\in W^{c}\) and \(@_{{\Gamma }_{0}}\in v^{c}(i)\) for all \(i\in \mathcal {F}\): The former is shown in Lemma 12.(1) and the latter is a consequence of Lemma 12.(2) and the definition of vc.
-
⊕c is idempotent, associative, and commutative: All these properties of ⊕c follow from its definition and Ax8.
□
In order to prove an appropriate Truth Lemma, we need the following auxiliary lemmas.
Lemma 14
For all\(\varphi \in \mathcal {EL}_{-}^{*}\), tc(φ) = [φ].
Proof
Let \(\varphi \in \mathcal {EL}_{-}^{*}\).
□
Lemma 15
For all Γ ∈ Wcand\(\varphi , \psi \in \mathcal {EL}_{-}^{*}\), \(t^{c}(\psi )\leq ^{c} t^{c}(\varphi )\)iff\(K_{\varphi }\overline {\psi }\in {\Gamma }\).
Proof
Let \({\Gamma }\in W^{c}\), and \(\varphi , \psi \in \mathcal {EL}_{-}^{*}\), and observe that
Suppose tc(ψ) ≤ctc(φ). Then, by the observation above, we have \(K_{\psi \wedge \varphi } \overline {\varphi }\), \(K_{\varphi }\overline {(\psi \wedge \varphi )}\)∈Γ. By Ax8, we also have that \(K_{\psi \wedge \varphi }\overline {\psi }\in {\Gamma }\). Then, \(K_{\psi \wedge \varphi }\overline {\psi } \wedge K_{\varphi }\overline {(\psi \wedge \varphi )}\in {\Gamma }\). Thus, by Ax6, we obtain that \(K_{\varphi }\overline {\psi }\in {\Gamma }\). For the other direction, suppose that \(K_{\varphi }\overline {\psi }\in {\Gamma }\). By Ax8, we also have \(K_{\varphi }\overline {\varphi }\in {\Gamma }\). Therefore, by Ax7, we obtain that \(K_{\varphi }\overline {(\psi \wedge \varphi )}\in {\Gamma }\). By Ax8, we already have that \(K_{\psi \wedge \varphi } \overline {\varphi }\in {\Gamma }\). Therefore, following the same steps above, we obtain that tc(ψ) ≤ctc(φ). □
Lemma 16 (Existence Lemma for \(\Box \))
For every mcs\({\Gamma }\in \mathcal {X}\)and\(\varphi \in \mathcal {EL}_{-}^{*}\), if \(\Box \varphi \not \in {\Gamma }\)then there is a mcs Δ such that\({\Gamma }\sim _{\Box } {\Delta }\)andφ∉Δ.
Proof
Standard, see, e.g., [8, Lemma 4.20]. □
Lemma 17 (Truth Lemma)
Let Γ0be a mcs ofEL∗and\({\mathcal{M}}^{c}= \langle W^{c}, @_{{\Gamma }_{0}}, \mathbb {T}^{c}, \oplus ^{c}, v^{c}, t^{c} \rangle \)be the canonical model for Γ0. Then, for all Γ ∈ Wc and \(\varphi \in \mathcal {EL}_{-}^{*}\),
Proof
The proof is by induction on the structure of φ. The cases for the atomic formulae, Booleans, and \(\Box \psi \) are standard, where the case for \(\Box \psi \) uses Lemma 16. Toward showing the cases for φ := Kψχ and φ := Aψ, suppose inductively that the statement holds for ψ and χ.
Case φ := Kψχ:
Case φ := Aψ:
□
Corollary 18
EL∗is a sound and complete axiomatization of\(\mathcal {EL}_{-}^{*}\)with respect to the class of epistemic models.
Proof
We prove only completeness since soundness is a matter of routine validity check. Let \(\not \vdash _{\mathsf {EL}^{*}}\varphi \). This means that {¬φ} is consistent, and by Lemma 9, can be extended to a mcs Γ0. Then, by Lemma 17, we obtain that \({\mathcal{M}}^{c}, {\Gamma }_{0}\not \vDash \varphi \), where \({\mathcal{M}}^{c}\) is the canonical model for Γ0. □
2.1.1 B.1.1 The (static) Logic of Knowledge Over \(\mathcal {EL}^{+}_{-}\)
We now provide a sound and complete axiomatization for the fragment \(\mathcal {EL}^{+}_{-}\) of \(\mathcal {EL}^{*}_{-}\) without the actuality operator.
Theorem 19
EL+given in Table 2is a sound and complete axiomatization of\(\mathcal {EL}^{+}_{-}\)with respect to the class of epistemic models.
The proof of Theorem 19 follows similarly to the proof of Corollary 18 except that we need to replace Lemma 10 by the following lemma.
Lemma 20
For all\({\Gamma }\in \mathcal {X}\), there exists a\(@_{\Gamma }\in \mathcal {X}\)such that\({\Gamma } \sim _{\Box } @_{\Gamma }\)and\(1\wedge {\dots } \wedge n\in @_{\Gamma }\).
Proof
Let \({\Gamma }\in \mathcal {X}\). Consider the set \(\{\varphi \in \mathcal {EL}^{+}_{-} : \Box \varphi \in {\Gamma }\}\cup \{1\wedge {\dots } \wedge n\}\) and suppose it is inconsistent. This implies that there are finitely many \(\varphi _{1}, \dots , \varphi _{k}\in \{\varphi \in \mathcal {EL}^{+}_{-} : \Box \varphi \in {\Gamma }\}\) such that \(\vdash _{\mathsf {EL}^{+}} (\varphi _{1}\wedge {\dots } \wedge \varphi _{k})\supset \neg (1\wedge {\dots } \wedge n)\). Then, by \(\mathsf {S5}_{\Box }\), we obtain \(\vdash _{\mathsf {EL}^{+}} (\Box \varphi _{1}\wedge {\dots } \wedge \Box \varphi _{k})\supset \Box \neg (1\wedge {\dots } \wedge n)\). As each \(\Box \varphi _{i}\in {\Gamma }\) for 1 ≤ i ≤ k, by Lemma 8, we have \(\Box \neg (1\wedge {\dots } \wedge n)\in {\Gamma }\). This means that \(\neg \Diamond (1\wedge {\dots } \wedge n)\in {\Gamma }\), contradicting consistency of Γ due to Ax1 and Lemma 8.(3). Therefore, by Lemma 9, \(\{\varphi \in \mathcal {EL}^{+}_{-} : \Box \varphi \in {\Gamma }\}\cup \{1\wedge {\dots } \wedge n\}\) extends to a \(\mathcal {EL}^{+}_{-}\)-maximally consistent set @Γ such that \(1\wedge {\dots } \wedge n\in @_{\Gamma }\). As \(\{\varphi \in \mathcal {EL}^{+}_{-} : \Box \varphi \in {\Gamma }\}\subseteq @_{\Gamma }\), we also have \({\Gamma }\sim _{\Box } @_{\Gamma }\). □
Lemma 20 guarantees the existence of an appropriate actual world \(@_{{\Gamma }_{0}}\) in the canonical model for a maximally EL+-consistent set Γ0.
2.2 B.2 The Logic of Knowledge Update Over \(\mathcal {EL}^{*}\)
This section presents soundness and completeness results for the dynamic language \(\mathcal {EL}^*\) of epistemic update. We axiomatize two classes of epistemic update models that represent maximal and minimal knowledge updates, respectively. These are the two extreme cases that an epistemic update function μ (given in Definition 1) can interpret: the former is modelled similarly to the so-called public announcements [25, 49, 50], and the latter represents an agent who learns the new piece of information without merging its intension with her prior information state.
Definition 4 (Maximal Epistemic Update Model)
A maximal epistemic update model is a tuple \({\mathcal{M}}= \langle W, @, \mathbb {T}, \oplus , \mu , v, t \rangle \) where \(\langle W, @, \mathbb {T}, \oplus , v, t \rangle \) is an epistemic model and \(\mu : \mathbb {I}_{@} \times \mathbb {I}_{@} \to \mathbb {I}_{@}\) is an update function such that μ(P,Q) = P ∩ Q.
Theorem 21
A sound and complete axiomatization\(\mathsf {EUL}^{*}_{\max \limits }\) of \(\mathcal {EL}^*\)with respect to the class of maximal epistemic update models is obtained by adding toEL∗the set of axioms and rules in Table 3.
Definition 5 (Minimal Epistemic Update Model)
A minimal epistemic update model is a tuple \({\mathcal{M}}= \langle W, @, \mathbb {T}, \oplus , \mu , v, t \rangle \) where \(\langle W, @, \mathbb {T}, \oplus , v, t \rangle \) is an epistemic model and \(\mu : \mathbb {I}_{@} \times \mathbb {I}_{@} \to \mathbb {I}_{@}\) is an update function such that μ(P,Q) = Q.
Theorem 22
A sound and complete axiomatization\(\mathsf {EUL}^{*}_{min}\)of\(\mathcal {EL}^*\)with respect to the class of minimal epistemic update models is obtained by replacing axiom (Ri) in Table 3by
2.2.1 B.2.1 Proofs of Theorems 21 and 22
The proofs of Theorems 21 and 22 are by the so-called standard DEL-technique completeness via reduction (or translation), as briefly explained in Section 4.4. For a detailed presentation of completeness by reduction, we refer the reader to [62, Chapter 7.4].
Definition 6 (Complexity measure for \(\mathcal {EL}^*\))
The complexity c(φ) of a formula \(\varphi \in \mathcal {EL}^*\) is a natural number recursively defined as
where \(|\mathcal {A}\mathcal {T}(\varphi )|\) is the number of elements in \(\mathcal {A}\mathcal {T}(\varphi )\).
Lemma 23
For all\(\varphi , \psi , \chi \in \mathcal {EL}^*\)and\(i, x\in \mathcal {A}\mathcal {T}\),
-
(1)
c(φ) > c(ψ) ifψis a proper subformula ofφ,
-
(2)
\(c([i: \varphi ] i) > c(A\varphi \supset (i\wedge \varphi ))\),
-
(3)
\(c([i: \varphi ] x) > c(A\varphi \supset (x\wedge (i\vee \neg i)))\), for i≠x
-
(4)
\(c([i: \varphi ] \neg \psi ) > c(A\varphi \supset \neg [i: \varphi ] \psi )\),
-
(5)
c([i : φ](ψ ∧ χ)) > c([i : φ]ψ ∧ [i : φ]χ),
-
(6)
\(c([i: \varphi ] \Box \psi ) > c(A\varphi \supset \Box [i: \varphi ] \psi )\),
-
(7)
\(c([i: \varphi ] A\psi ) > c(A\varphi \supset A[i: \varphi ] \psi )\),
-
(8)
\(c([i: \varphi ] K_{\psi }\chi ) > c(A\varphi \supset (K_{\psi }\overline {\chi } \wedge \Box [i: \varphi ](\psi \supset \chi ))) \),
-
(9)
\(c([i: \varphi ] K_{\psi }\chi ) > c(A\varphi \supset (K_{\psi \wedge \varphi }\overline {\chi } \wedge \Box [i: \varphi ](\psi \supset \chi )))\),
-
(10)
\(c([i: \varphi ] K_{\psi }\chi ) > c(A\varphi \supset (K_{\psi }\overline {(\chi \wedge \varphi )} \wedge \Box [i: \varphi ](\psi \supset \chi )))\),
-
(11)
\(c([i: \varphi ] K_{\psi }\chi ) > c(A\varphi \supset (K_{\psi \wedge \varphi }\overline {(\chi \wedge \varphi )} \wedge \Box [i: \varphi ](\psi \supset \chi )))\).
Proof
Follows by easy calculations using Definition 6. And, obviously, (8)–(10) follow from (11). □
Definition 7 (Translation \(f: \mathcal {EL}^* \rightarrow \mathcal {EL}_{-}^{*}\))
The translation \(f: \mathcal {EL}^* \rightarrow \mathcal {EL}_{-}^{*}\) is defined as follows:
We need the following lemma in order to be able to use the derived replacement of equivalents rule given in Theorem 7.(1) in the completeness proofs of \(\mathsf {EUL}^{*}_{\max \limits }\) and \(\mathsf {EUL}^{*}_{min}\). For this lemma to go through, it is crucial that the reduction axioms Ri and Rx≠i have occurrences of each element in \(\mathcal {A}\mathcal {T}(\varphi )\) and i on the right-hand-side of the equivalences, where φ is the sentence inside the dynamic operator and i is the updated frame of mind.
Lemma 24
For all\(\varphi \in \mathcal {EL}^*\), \(\mathcal {A}\mathcal {T}(\varphi )=\mathcal {A}\mathcal {T}({f(\varphi )})\).
Proof
The proof follows by an easy c-induction on the structure of φ and uses Lemma 23. Note that the case for φ := [i : ψ]χ requires subinduction on χ. □
Lemma 25
For all\(\varphi \in \mathcal {EL}^*\), \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} \varphi \equiv f(\varphi )\).
Proof
The proof follows by c-induction on the structure of φ and uses Lemma 23. Cases for the atomic formulae, the Boolean connectives, and \(\Box \) are elementary. Here we only show the cases for φ := Kψχ and φ := [i : ψ]χ, where the latter requires subinduction on χ. Suppose inductively that \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} \psi \equiv f(\psi )\), for all ψ with c(ψ) < c(φ).
Case φ := Kψχ
By Lemma 23.(1) and the induction hypothesis (IH), we have \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} \psi \equiv f(\psi )\). Moreover, by Lemma 24, we have \(\mathcal {A}\mathcal {T}(\psi )=\mathcal {A}\mathcal {T}({f(\psi )})\). Therefore, by Ax8 in Table 1, we obtain \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} K_{\psi }\overline {f(\psi )}\) and \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} K_{f(\psi )}\overline {\psi }\). Then, by Theorem 7.(1), we obtain \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} K_{\psi }\chi \equiv K_{f(\psi )}\chi \). Similarly, we also have \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} \chi \equiv f(\chi )\) and \(\mathcal {A}\mathcal {T}(chi)=\mathcal {A}\mathcal {T}({f(\chi )})\), thus, \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} K_{\chi }\overline {f(\chi )}\) and \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} K_{f(\chi )}\overline {\chi }\). Then, by Theorem 7.(1) again, we obtain \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} K_{f(\psi )}\chi \equiv K_{f(\psi )} f(\chi )\). Therefore, by CPL, we conclude that \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} K_{\psi }\chi \equiv K_{f(\psi )} f(\chi )\), with Kf(ψ)f(χ) = f(Kψχ) by Definition 7.
Case φ := [i : ψ]χ: we prove only the cases χ := x with x≠i, and χ := [j : 𝜃]α. All the other cases follow similarly by using the corresponding reduction axioms, Lemma 23, and Definition 7.
Subcase χ := x, for x≠i
-
1.
\(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} [i: \psi ]x \equiv (A\varphi \supset (x\wedge (i\vee \neg i))) \qquad \qquad \qquad ~~~~ R_{x\not =i}\)
-
2.
\(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} (A\varphi \supset (x\wedge (i\vee \neg i)))\equiv f(A\varphi \supset (x\wedge (i\vee \neg i))) ~~~~\text {Lemma} 23.(3), IH\)
And, \(f(A\varphi \supset (x\wedge (i\vee \neg i))) =f([i: \psi ]x )\) by Definition 7.
Subcase χ := [j : 𝜃]α By Lemma 23.(1) and IH, we know that ⊩ [j : 𝜃]α ≡ f([j : 𝜃]α)
-
1
\(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} [j: \theta ]\alpha \equiv f([j: \theta ]\alpha )\) Lemma 23.(1), IH
-
2
\( \vdash _{\mathsf {EUL}^{*}_{\max \limits }} [i: \psi ]([j: \theta ]\alpha \equiv f([j: \theta ]\alpha ))\) Nec[]
-
3.
\( \vdash _{\mathsf {EUL}^{*}_{\max \limits }} [i: \psi ][j: \theta ]\alpha \equiv [i: \psi ]f([j: \theta ]\alpha )\) R¬, R∧
-
4.
\( \vdash _{\mathsf {EUL}^{*}_{\max \limits }} [i: \psi ]f([j: \theta ]\alpha ) \equiv f([i: \psi ]f([j: \theta ]\alpha ))\) IH
-
5
\( \vdash _{\mathsf {EUL}^{*}_{\max \limits }} [i: \psi ][j: \theta ]\alpha \equiv f([i: \psi ]f([j: \theta ]\alpha ))\) 3, 4, CPL
And, f([i : ψ]f([j : 𝜃]α)) = f([i : ψ][j : 𝜃]α) by Definition 7. □
Proof of Theorem 21
Let \(\varphi \in \mathcal {EL}^*\) such that \(\not \vdash _{\mathsf {EUL}^{*}_{\max \limits }} \varphi \). By Lemma 25, there is \(\psi \in \mathcal {EL}_{-}^{*}\) such that \(\vdash _{\mathsf {EUL}^{*}_{\max \limits }} \varphi \equiv \psi \). Therefore, \(\not \vdash _{\mathsf {EUL}^{*}_{\max \limits }} \psi \). As \(\psi \in \mathcal {EL}_{-}^{*}\) and \(\mathsf {EL}^{*}\subseteq \mathsf {EUL}^{*}_{\max \limits }\), we also have \(\not \vdash _{\mathsf {EL}^{*}}\psi \). Then, by Corollary 18, there is an epistemic model \({\mathcal{M}}=\langle W, @, \mathbb {T}, \oplus , v, t \rangle \) and w ∈ W such that \({\mathcal{M}}, w\not \vDash \psi \). Observe that the tuple \(\langle W, @, \mathbb {T}, \oplus , \mu , v, t\rangle \), where \(\mu : \mathbb {I}_{@} \times \mathbb {I}_{@} \to \mathbb {I}_{@}\) such that μ(P,Q) = P ∩ Q, is a maximal epistemic update model. Then, by Lemma 5, we have \(\langle W, @, \mathbb {T}, \oplus , \mu , v, t\rangle , w\not \vDash \psi \). Therefore, by the soundness of \(\mathsf {EUL}^{*}_{\max \limits }\) with respect to maximal epistemic update models, we obtain that \(\langle W, @, \mathbb {T}, \oplus , \mu , v, t\rangle , w\not \vDash \varphi \). □
Proof of Theorem 22
Follows the same steps as the proof of Theorem 21. We need to replace every occurrence of \([i: \varphi ] i \equiv A\varphi \supset (i\wedge \varphi )\) by \([i: \varphi ] i \equiv A\varphi \supset (\varphi \wedge (i\vee \neg i))\). □
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Hawke, P., Özgün, A. & Berto, F. The Fundamental Problem of Logical Omniscience. J Philos Logic 49, 727–766 (2020). https://doi.org/10.1007/s10992-019-09536-6
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-019-09536-6