A GENUINELY UNTYPED EXPLANATION OF COMMON BELIEF AND KNOWLEDGE

Abstract

This paper provides a consistent first-order theory solving the knower paradoxes of Kaplan and Montague, with the following main features: 1. It solves the knower paradoxes by providing a faithful formalization of the principle of veracity (that knowledge requires truth), using both a knowledge and a truth predicate. 2. It is genuinely untyped i.e., it is untyped not only in the sense that it uses a single knowledge predicate applying to all sentences in the language (including sentences in which this predicate occurs), but in the sense that its axioms quantify over all sentences in the language, thus supporting comprehensive reasoning with untyped knowledge ascriptions. 3. Common knowledge predicates can be defined in the system using self-reference. These facts, together with a technique based on Löb’s theorem, enables it to support comprehensive reasoning with untyped common knowledge ascriptions (without having any axiom directly addressing common knowledge).

1 Introduction

In [14], Kaplan and Montague showed that certain intuitive axioms for a first-order theory of knowledge, formalized as a predicate, are jointly inconsistent. A similar result was established by Montague in [18]. Both arguments rely on self-referential sentences that are expressible in untyped systems. I offer a system of belief, $\mathsf {DCB}$ , which explains common belief, and which extends to a system of knowledge, $\mathsf {KT}$ , offering a compelling approach to overcome these knower paradoxes. They have the following significant features:

1. 1. First-order: The systems are expressed as first-order extensions of Peano Arithmetic. Thus they benefit from the many desirable properties of first-order logic, as well as the expressive and deductive power of Peano Arithmetic, and its foundational role for mathematics and science.

2. 2. Faithful formalizations: The axioms are straight-forward formalizations of the relevant epistemic principles. In particular, $\mathsf {KT}$ resolves the knower paradoxes by providing a faithful formalization of the principle of veracity (that knowledge requires truth), using both a knowledge and a truth predicate.

3. 3. Deductive closure: $\mathsf {DCB}$ proves that belief/knowledge is deductively closed in certain precise senses, ¹ leveraging an innovative self-referential reflection axiom, $\mathsf {R}_{\mathsf {DCB}}$ .

4. 4. Genuinely untyped: They are untyped not only in the sense that they use a single belief/knowledge predicate applying to all sentences in the language (including sentences in which this predicate occurs), but in the sense that their axioms quantify over all sentences in the language, thus supporting comprehensive reasoning with untyped belief/knowledge ascriptions. Moreover, their self-referential reflection axiom, $\mathsf {R}_{\mathsf {DCB}}$ , makes essential use of the expressive power of the untyped approach. The formulation of this axiom is central to the results of this paper, as it both enables the explanation of common knowledge and is validated by the revision semantics, as detailed below.

5. 5. Explanation of common knowledge: Common belief/knowledge predicates can be defined in the systems as fixed points. This fact, together with the formulation of the reflection axiom $\mathsf {R}_{\mathsf {DCB}}$ , which combines with a technique based on Löb’s theorem, enables comprehensive reasoning with untyped common belief/knowledge ascriptions. Note that this is achieved without having any axiom directly addressing common belief/knowledge.

6. 6. Revision semantics: $\mathsf {KT}$ has a revision semantics generalizing the usual revision semantics for the truth predicate (following Stern’s [20]). The key to obtaining this result for $\mathsf {KT}$ is that the reflection axiom, $\mathsf {R}_{\mathsf {DCB}}$ , can be validated in the revision semantics. It follows that $\mathsf {KT}$ and its sub-system $\mathsf {DCB}$ are consistent.

§2 sets the notation used throughout the paper and specifies the language and basic assumptions on the theories considered. It also briefly explains Gödel’s implementation of syntax, and formally states the knower paradoxes of Kaplan and Montague.

The system of belief, $\mathsf {DCB}$ , is introduced in §3. $\mathsf {DCB}$ is a simple and robust formalization of untyped deductively closed belief. A key axiom is its self-referential reflection axiom, $\mathsf {R}_{\mathsf {DCB}}$ , asserting that anything internally provable in the system is believed by all agents. Common belief is definable in $\mathsf {DCB}$ using Gödel’s fixed point lemma. A technique based on Löb’s theorem is employed to establish a number of positive results on these defined common belief predicates. Two highlights are Corollary 4, establishing that they are unique, and Theorem 9, establishing that they enjoy the same deductive closure properties as the primitive belief predicate.

In §4, $\mathsf {DCB}$ is extended to the system $\mathsf {KT}$ of knowledge and truth. A fundamental design choice, motivated by the desire to obtain a genuinely untyped system, is that $\mathsf {KT}$ is axiomatized as an extension of the Friedman–Sheard system of truth ( $\mathsf {FS}$ , introduced in [5]). Thus, I follow a general approach developed by Stern in [20] to formalize modalities as predicates. Halbach showed in [9] that $\mathsf {FS}$ is locally validated by the revision semantics of Gupta and Herzberger (from [7, 11, 12]), in the sense that every finite fragment of $\mathsf {FS}$ is satisfied by an expansion of the standard model of arithmetic obtained by a finite number of such revisions of the interpretation of the truth predicate. In [20], Stern extended the revision semantics to necessity, treated as a first-order predicate rather than as a modal operator. In §4, I utilize Stern’s technique to develop a revision semantics for multi-agent knowledge. This approach generalizes Hintikka’s possible worlds approach from [13], and is thus coherent with that tradition. The consistency of $\mathsf {KT}$ comes out as a corollary of Theorem 15, which shows that a certain extension of $\mathsf {KT}$ is locally modeled by this revision semantics. The key insight leading up to Theorem 15 is that the reflection axiom $\mathsf {R}_{\mathsf {DCB}}$ can be validated in the revision semantics. This fact is encapsulated in Lemmata 13 and 14.

§5 discusses the approach of this paper and compares it to other approaches in the literature.

In summary, this paper introduces a genuinely untyped predicate approach to epistemic logic, which explains common knowledge. The ensuing system of knowledge does not merely overcome the knower paradoxes; it makes use of untyped resources to efficiently define and explain common knowledge, and it is validated by a revision semantics generalizing the traditional Hintikka semantics of epistemic logic.

2 Preliminaries

Let L be a first-order language. An L-system is defined as a recursively enumerable set of L-sentences that includes (a Hilbert-style) axiomatization of first-order logic and is closed under modus ponens. For convenience first-order systems are assumed to include the propositional constants $\top $ and $\bot $ along with axioms asserting that these formalize truth and falsity, respectively. Each system is given as a list of axioms and deductive rules, such as the deductive rule $\mathsf {NEC}^{\mathrm {K}}$ :

(NEC ^K) $$\begin{align} \vdash \phi \phantom{~~} \Longrightarrow \phantom{~~} \vdash \mathrm{K}(\ulcorner \phi \urcorner). \end{align} $$

Here $\mathrm {K}$ is a knowledge predicate, and $\mathsf {NEC}^{\mathrm {K}}$ is the deductive rule that if $\phi $ is a theorem of the system, then so is $\mathrm {K}(\ulcorner \phi \urcorner )$ . Note that if a system S with a deductive rule, say $\mathsf {NEC}^{\mathrm {K}}$ , is extended to a system $S'$ , then $\mathsf {NEC}^{\mathrm {K}}$ can be applied in $S'$ to any theorem of $S'$ . On the other hand, $\mathsf {NEC}^{\mathrm {K}}$ can generally not be applied in S to theorems of $S'$ ; in other words, it cannot be applied to undischarged assumptions, so it cannot in general be used to derive $\phi \rightarrow \mathrm {K}(\ulcorner \phi \urcorner )$ , for a sentence $\phi $ .

I employ the following notation, for any arity $n \in \mathbb {N}$ :

$$ \begin{align*} \mathrm{Var} &=_{\mathrm{df}} \text{the set of variables.} \\ L^n &=_{\mathrm{df}} \text{the set of } L\text{-formulas with precisely } n \text{ free variables.} \\ L^n[v_1, \cdots, v_n] &=_{\mathrm{df}} \text{ the set of } L\text{-formulas with precisely } v_1, \cdots, v_n \text{ as free variables.} \\ \mathrm{Atom}_L^n &=_{\mathrm{df}} \text{the set of atomic } L\text{-formulas with precisely } n \text{ free variables.} \\ \mathrm{Term}_L^n &=_{\mathrm{df}} \text{the set of } L\text{-terms with precisely } n \text{ free variables.} \end{align*} $$

When the superscript n above is dropped, all arities are included, e.g., $\mathrm {Term}_L$ is the set of all L-terms. The substitution function, denoted $\mathrm {sbt} : L \times \mathrm {Term}_{\mathcal {L}} \times \mathrm {Var} \rightarrow \mathcal {L}$ , maps $\langle \phi , t, v \rangle $ to the formula obtained from $\phi $ by substituting every instance of the variable v by the term t.

Let $\mathcal {L}$ be the first-order language with the usual symbols $\underline {0}, S, +, \cdot $ of arithmetic, a unary predicate symbol U, a unary function symbol u, a unary predicate symbol $\mathrm {K}^1$ , a binary relation symbol $\mathrm {K}^2$ , a unary predicate symbol $\mathrm {T}$ , and a unary predicate symbol $\mathrm {Ag}$ . When the arity is clear from the context, $\mathrm {K}^1$ and $\mathrm {K}^2$ will both be denoted $\mathrm {K}$ . The sublanguage of $\mathcal {L}$ generated by the arithmetical symbols is denoted $\mathcal {L}_{\mathsf {PA}}$ and the sublanguage generated by $\underline {0}, S, \cdot , \times , U, u, \mathrm {Ag}$ is denoted $\mathcal {L}_-$ . All the systems of the paper are formulated as extensions of Peano Arithmetic ( $\mathsf {PA}$ ) in $\mathcal {L}$ , or a sublanguage thereof. The standard $\mathcal {L}_{\mathsf {PA}}$ -model of arithmetic is denoted $\mathbb {N}$ .

$\mathrm {K}(x, y)$ is intended to express “the agent x knows the sentence y”. $\mathrm {K}(y)$ is intended to express “we know y”, or suchlike. $\mathrm {T}(y)$ is intended to express “y is true”. $\mathrm {Ag}(x)$ is intended to express “x is an agent”. Utilizing the method of coding in arithmetic, the symbols $U, u$ are employed as universal relation and function symbols, available for the sake of generality, ensuring that the systems considered can be seamlessly extended to apply to any recursively enumerable language. ²

As is familiar, Gödel showed in [8] how to implement syntactical resources in arithmetic. Here follows some notation and basic properties of this machinery: For any $n \in \mathbb {N}$ , $\mathrm {num}(n)$ (or $\underline {n}$ ) denotes the numeral $S^n(\underline {0}) \in \mathrm {Term}_{\mathcal {L}_{\mathsf {PA}}}^0$ . Let $t \in \mathrm {Term}_{\mathcal {L}}$ and $\phi \in \mathcal {L}$ . The Gödel quotes $\mathrm {gq}(t)$ (or $\ulcorner t \urcorner $ ) and $\mathrm {gq}(\phi )$ (or $\ulcorner \phi \urcorner $ ) denote numerals which represent t and $\phi $ , respectively, in arithmetic. For example, if $\phi \in \mathcal {L}^0$ , then $\mathrm {K}(x, \ulcorner \phi \urcorner )$ expresses “x knows ‘ $\phi $ ’”. Closely related to these are the Gödel codes $\mathrm {gc}(t), \mathrm {gc}(\phi )$ of t and $\phi $ , respectively, which are the numbers in the standard model interpreting $\mathrm {gq}(t), \mathrm {gq}(\phi )$ , respectively.

In order to conveniently utilize Gödel’s machinery, the systems considered in this paper are formulated as extensions of a base system, $\mathsf {Base}$ . One can get by with Robinson’s arithmetic ( $\textsf {Q}$ ) as base system for syntactic purposes. But since proof by induction is so natural, I require that $\mathsf {Base}$ proves all the theorems of $\mathsf {PA}(\mathcal {L})$ , which I axiomatize as $\mathsf {PA}$ with its induction schema extended to $\mathcal {L}$ . I also require that $\mathsf {Base}$ has axioms for the various representations involved in the Gödel machinery, which I now proceed to explain:

Let $\phi \in \mathcal {L}^n$ , let $R(x_1, \cdots , x_n)$ be a relation on $\mathbb {N}$ and let S be an $\mathcal {L}$ -system. $\phi $ represents R in S if for all $a_1, \cdots , a_n \in \mathbb {N}$ ,

$$ \begin{align*} R(a_1, \cdots, a_n) \Longleftrightarrow S \vdash \phi(\underline{a_1}, \cdots, \underline{a_n}). \end{align*} $$

Representation of functions is analogously defined. $\mathsf {Base}$ is assumed to be equipped with various function and relation symbols, representing various syntactically relevant functions and relations. Formally, these symbols are implemented by means of U and u as explained above, and by means of axioms of $\mathsf {Base}$ asserting what relation or function each such symbol represents. These representations are denoted with a dot under the name of the relation/function in question. For example, denotes the representation of $\mathcal {L}^0$ , and represents a function from $\mathcal {L} \times \mathcal {L}$ to $\mathcal {L}$ mapping two formulas to their conjunction. The evaluation function returning the numeric value of any closed $\mathcal {L}_{\mathsf {PA}}$ -term is denoted $\mathrm {ev} : \mathrm {Term}_{\mathcal {L}_{\mathsf {PA}}}^0 \rightarrow \mathbb {N}$ . Its representation is also denoted $x^\circ $ . Moreover, for any recursive system S, there is a formula $\Pr _S$ in L that adequately represents provability in S, in the precise sense that it satisfies the well-known Hilbert–Bernays provability conditions.

Since $\mathsf {Base} \vdash \mathsf {PA}$ , Gödel’s fixed point lemma is available in $\mathsf {Base}$ , facilitating formalization of self-reference. More precisely, for any $\phi (x_1, \cdots , x_{n+1}) \in \mathcal {L}^{n+1}$ there is a formula $\theta (x_1, \cdots , x_n) \in \mathcal {L}^n$ , such that

$$ \begin{align*} \mathsf{Base} \vdash \forall x_1, \cdots, x_n \big( \theta(x_1, \cdots, x_n) \leftrightarrow \phi(x_1, \cdots, x_n, \ulcorner \theta \urcorner) \big). \end{align*} $$

The Gödel machinery enables us to formalize statements about knowledge, for example the statement that the knowledge of each agent is closed under modus ponens:

In order to make such statements more readable, I introduce the following abbreviations, for any formula $\phi $ in one free variable, and any formula $\psi $ :

$$ \begin{align*} \forall x \in \phi \hspace{2pt} \big( \psi(x) \big) &\text{ abbreviates } \forall x \big(\phi(x) \rightarrow \psi(x)\big) \\ \exists x \in \phi \hspace{2pt} \big( \psi(x) \big) &\text{ abbreviates } \exists x \big(\phi(x) \wedge \psi(x)\big) \\ \forall x_1, \cdots x_n \psi &\text{ abbreviates } \forall x_1 \cdots \forall x_n \psi \\ \exists x_1, \cdots x_n \psi &\text{ abbreviates } \exists x_1 \cdots \exists x_n \psi. \end{align*} $$

These abbreviations may also be combined. For example, the above sentence is written as follows:

In this context, the knower paradoxes of Kaplan and Montague can be stated as follows.

Theorem (Kaplan & Montague, 1960).

The $\mathcal {L}$ -theory extending $\mathsf {PA}$ with the following axiom schemata is inconsistent, where $\phi , \psi $ range over sentences in $\mathcal {L}$ :

(UT ^K) $$\begin{align} & \mathrm{K}(\ulcorner \phi \urcorner) \rightarrow \phi \end{align} $$

(K[UT ^K]) $$\begin{align} & \mathrm{K}(\ulcorner \mathrm{K}(\ulcorner \phi \urcorner) \rightarrow \phi \urcorner) \end{align} $$

(I ^K) $$\begin{align} & {\Pr}_{\mathsf{PA}}(\ulcorner \phi \rightarrow \psi \urcorner) \wedge \mathrm{K}(\ulcorner \phi \urcorner) \rightarrow \mathrm{K}(\ulcorner \psi \urcorner). \end{align} $$

Theorem (Montague, 1963).

The $\mathcal {L}$ -theory extending $\mathsf {PA}$ with the following axiom schema and deductive rule is inconsistent, where $\phi $ ranges over sentences in $\mathcal {L}$ :

(UT ^K) $$\begin{align} & \mathrm{K}(\ulcorner \phi \urcorner) \rightarrow \phi \end{align} $$

(NEC ^K) $$\begin{align} & \vdash \phi \phantom{~~} \Longrightarrow \phantom{~~} \vdash \mathrm{K}(\ulcorner \phi \urcorner). \end{align} $$

$\mathsf {UT}^{\mathrm {K}}$ formalizes the classical philosophical principle of veracity (that knowledge requires truth) and stands for Untyped T axiom for $\mathrm {K}$ (as it is an untyped analog of the axiom $\mathsf {T}$ from modal logic); $\mathsf {NEC}^{\mathrm {K}}$ formalizes that deduction in the system is a legitimate method for generating knowledge and stands for Necessitation for $\mathrm {K}$ ; $\mathsf {I}^{\mathrm {K}}$ formalizes that knowledge is closed under deduction in $\mathsf {PA}$ and derives from notation in [14]. Note that $\mathrm {K}[\mathsf {UT}^{\mathrm {K}}]$ follows from a single application of $\mathsf {NEC}^{\mathrm {K}}$ to $\mathsf {UT}^{\mathrm {K}}$ . The proofs of these theorems rely on Gödel’s fixed point lemma. The former uses a sentence $\kappa $ , such that $\kappa \leftrightarrow \mathrm {K}(\neg \kappa )$ , while the latter uses a sentence , such that .

3 A system of belief explaining common belief

In this section I introduce the $\mathcal {L}$ -system $\mathsf {DCB}$ (Deductively Closed Belief, axiomatized in Figure 1). It is intended as a simple and robust system formalizing belief as closed under deduction, which is still powerful enough to define common belief and prove that common belief is analogously closed under deduction.

Figure 1 Axioms of $\mathsf {DCB.}$

The predicate $\mathrm {K}$ is here used to formalize belief. In §4, $\mathsf {DCB}$ is extended to the system $\mathsf {KT}$ of knowledge and truth, in which $\mathrm {K}$ is used to formalize knowledge. Axiom $\mathrm {K}^1$ - $\mathrm {K}^2$ simply defines $\mathrm {K}^1(\phi )$ as expressing “every agent believes/knows $\phi $ ”. Axiom $\textsf {UK}^{\mathrm {K}}$ asserts that belief/knowledge is closed under modus ponens. Axiom $\mathsf {R}_{\mathsf {DCB}}$ (Reflection over $\mathsf {DCB}$ ) is an innovation of this paper that provides additional internally quantified deductive closure. It robustly expresses that belief/knowledge extends the basic provability predicate $\Pr _{\mathsf {DCB}}$ of $\mathsf {DCB}$ . This robustness is a consequence of that $\mathsf {R}_{\mathsf {DCB}}$ is itself an axiom of the system $\mathsf {DCB}$ , whose provability predicate it refers to. Thus $\mathsf {R}_{\mathsf {DCB}}$ formalizes a self-referential sentence, and its existence follows from the Gödel fixed point lemma. This is established as follows: Let S be the recursive system that extends $\mathsf {Base}$ with $\textsf {Non-triviality}$ , $\mathrm {K}^1$ - $\mathrm {K}^2$ , and $\textsf {UK}^{\mathrm {K}}$ . Let $\Pr _S$ be an arithmetic formula that adequately represents provability in S. Define $\Pr ^{\prime }_S(x, y)$ as . Then, for any $\mathcal {L}$ -sentence $\psi $ , we have that $\Pr ^{\prime }_S(\ulcorner \psi \urcorner , y)$ adequately represents provability in $S + \psi $ . Now, by the Gödel fixed point lemma, there is a sentence $\mathsf {R}_{\mathsf {DCB}}$ , such that

$\mathsf {DCB}$ is formally defined as S plus the fixed point sentence $\mathsf {R}_{\mathsf {DCB}}$ just obtained. Note that by the Hilbert–Bernays conditions, ${\Pr }^{\prime }_S(\ulcorner \mathsf {R}_{\mathsf {DCB}} \urcorner , y)$ adequately represents provability in $\mathsf {DCB}$ , and coherently defines $\Pr _{\mathsf {DCB}}$ . This justifies the succinct formulation of $\mathsf {R}_{\mathsf {DCB}}$ in Figure 1.

The consistency of $\mathsf {DCB}$ depends to some extent on the choice of its subsystem $\mathsf {Base}$ . Obviously, if $\mathsf {Base}$ is strangely chosen to include the negation of some axiom of $\mathsf {DCB}$ , then $\mathsf {DCB}$ will be inconsistent. Proposition 1 establishes that, for natural choices of $\mathsf {Base}$ , $\mathsf {DCB}$ is conservative over $\mathsf {Base}$ . A fairly general application of the framework is obtained by interpreting $\mathrm {Ag}(x)$ and $\mathrm {K}(x, y)$ by arithmetical formulas $\phi _{\mathrm {Ag}}(x)$ and $\phi _{\mathrm {K}}(x, y)$ , respectively. $\mathsf {Base}$ will typically be chosen so as to provide a foundational system to work in, which does not formalize any significant epistemic assumptions. Therefore, $\mathsf {Base} + \mathrm {Ag}(x) \leftrightarrow \phi _{\mathrm {Ag}}(x) + \mathrm {K}(x, y) \leftrightarrow \phi _{\mathrm {K}}(x, y)$ will typically be conservative over $\mathsf {Base}$ . A trivial application of $\mathsf {DCB}$ is obtained by formalizing one agent who believes every sentence; this suggests a simple interpretation of $\mathsf {DCB}$ in $\mathsf {Base}$ , for the case that $\mathsf {Base}$ is $\mathsf {PA}(\mathcal {L})$ . A minimal non-trivial application of $\mathsf {DCB}$ , formalizing one agent who believes precisely the theorems of $\mathsf {DCB}$ , is obtained by choosing $\phi _{\mathrm {Ag}}(x)$ to be $x = 0$ , and choosing $\phi _{\mathrm {K}}(x, y)$ to be $x = 0 \wedge \Pr _{\mathsf {DCB}}(y)$ . This application is here used to establish the conservativity of $\mathsf {DCB}$ over any sufficiently epistemically neutral choice of $\mathsf {Base.}$

Proposition 1. Let $\mathsf {Basic}_{\mathsf {DCB}}$ be the system $\mathsf {Base} + \mathrm {Ag}(x) \leftrightarrow x = 0 + \mathrm {K}^1(y) \leftrightarrow \Pr _{\mathsf {DCB}}(y) + \mathrm {K}^2(x, y) \leftrightarrow x = 0 \wedge \Pr _{\mathsf {DCB}}(y)$ .

1. (a) $\mathsf {Basic}_{\mathsf {DCB}}$ interprets $\mathsf {DCB}$ .

2. (b) If $\mathsf {Basic}_{\mathsf {DCB}}$ is conservative over $\mathsf {Base}$ , then $\mathsf {DCB}$ is conservative over $\mathsf {Base}$ .

3. (c) If $\mathsf {Base}$ is $\mathsf {PA}(\mathcal {L})$ , then $\mathsf {Base}$ interprets $\mathsf {DCB}$ .

Proof. (a): The interpretation is generated as follows: Any formula $\phi $ in the language excluding the symbols $\mathrm {Ag}$ , $\mathrm {K}^1$ , and $\mathrm {K}^2$ is interpreted by $\phi $ . $\mathrm {Ag}(x)$ is interpreted by $x = 0$ , $\mathrm {K}^2(x, y)$ is interpreted by $x = 0 \wedge \Pr _{\mathsf {DCB}}(y)$ , and $\mathrm {K}^1(y)$ is interpreted by $\Pr _{\mathsf {DCB}}(y)$ . We establish that the interpretations of the axioms of $\mathsf {DCB}$ are provable in $\mathsf {Basic}_{\mathsf {DCB}}$ : Observe that the additional axioms of $\mathsf {Basic}_{\mathsf {DCB}}$ over $\mathsf {Base}$ mirror the interpretation. Thus, $\mathsf {Basic}_{\mathsf {DCB}}$ proves $\phi $ iff $\mathsf {Basic}_{\mathsf {DCB}}$ proves the interpretation of $\phi $ . So the interpretations of the axioms of $\mathsf {Basic}_{\mathsf {DCB}}$ are provable in $\mathsf {Basic}_{\mathsf {DCB}}$ . The interpretations of $\textsf {Non-triviality}$ and $\mathrm {K}^1$ - $\mathrm {K}^2$ are immediately seen to be provable in $\mathsf {Basic}_{\mathsf {DCB}}$ , by definition of the interpretation. The interpretation of $\mathsf {UK}^{\mathrm {K}}$ asserts the closure of $\Pr _{\mathsf {DCB}}$ under modus ponens. It is provable in $\mathsf {Basic}_{\mathsf {DCB}}$ by one of the Hilbert–Bernays conditions. The interpretation of $\mathsf {R}_{\mathsf {DCB}}$ is trivially provable in $\mathsf {Basic}_{\mathsf {DCB}}$ .

(b): This follows immediately from (a).

(c): Assume that $\mathsf {Base}$ is $\mathsf {PA}(\mathcal {L})$ . Then $\mathsf {Base}$ interprets $\mathsf {Basic}_{\mathsf {DCB}}$ by the interpretation in (a). This is seen as follows: The interpretation of each induction axiom of $\mathsf {Base}$ is also an induction axiom of $\mathsf {Base}$ . The interpretations of the remaining axioms of $\mathsf {Basic}_{\mathsf {DCB}}$ are trivially provable in $\mathsf {Base}$ , since they mirror the interpretation. By combining this with (a), we obtain (c).

Although not included in $\mathsf {DCB}$ , the following supplementary axiom (Untyped Barcan Formula) will also be considered:

(UBF)

Let $\phi $ be an $\mathcal {L}$ -sentence, and suppose that $\mathsf {DCB} \vdash \phi $ . Then by a Hilbert–Bernays condition on the provability predicate, ³ $\mathsf {DCB} \vdash \Pr _{\mathsf {DCB}}(\ulcorner \phi \urcorner )$ . So by $\mathsf {R}_{\mathsf {DCB}}$ , we have $\mathsf {DCB} \vdash \mathrm {K}(\ulcorner \phi \urcorner )$ . Recall that the deductive rule, $\mathsf {DCB} \vdash \phi \Rightarrow \mathsf {DCB} \vdash \mathrm {K}(\ulcorner \phi \urcorner )$ , thus admitted by $\mathsf {DCB}$ is called $\mathsf {NEC}^{\mathrm {K}}$ .

The idealized deductive closure properties asserted by $\mathsf {DCB}$ are justified by the epistemological importance of deduction in expanding belief and knowledge, by their conceptual simplicity, and by their methodological merits. The latter are show-cased in the rest of this section, which establishes that $\mathsf {DCB}$ defines common belief and proves that it has all the deductive closure properties that its axioms assert for belief. The proofs utilize a technique based on Löb’s theorem.

Let $A(x)$ be an $\mathcal {L}$ -formula with only x free. I write $\mathrm {CK}_A(y)$ (read Common Belief for the agents satisfying A) for an $\mathcal {L}$ -formula with only y free, such that

(CBE)

I call this the Common Belief Equivalence. It follows from Gödel’s fixed point lemma that there is a formula $\mathrm {CK}_A(y)$ satisfying ( $\mathsf {CBE}$ ). It is convenient to abbreviate $\textsf {CBE}$ as follows:

where $\Psi _A(u, v)$ is the formula

Let me pause to explain why $\mathrm {CK}_A$ (in the context of $\mathsf {DCB}$ ) is a plausible formalization of common belief for the agents satisfying A. Consider e.g., how common knowledge is introduced in [4, chap. 1]: “In some cases we also need to consider the state in which simultaneously everyone knows a fact $\phi $ , everyone knows that everyone knows $\phi $ , everyone knows that everyone knows that everyone knows $\phi $ , and so on. In this case we say that the group has common knowledge of $\phi $ .” Reasoning in $\mathsf {DCB}$ , let $\phi $ be an $\mathcal {L}$ -sentence, let $\alpha $ be an agent, such that $A(\alpha )$ , and assume that $\mathrm {CK}_A(\ulcorner \phi \urcorner )$ . The $\rightarrow $ direction of ( $\mathsf {CBE}$ ) now yields: First, $\mathrm {K}(\alpha , \ulcorner \phi \urcorner )$ and $\mathrm {K}(\alpha , \ulcorner \mathrm {CK}_A(\ulcorner \phi \urcorner ) \urcorner )$ . Second, applying deductive closure to the latter, $\mathrm {K} (\alpha , \ulcorner \forall x \in \mathrm {Ag} \hspace {2pt} \big ( A(x) \rightarrow \mathrm {K}(x, \ulcorner \phi \urcorner ) \big ) \urcorner )$ and $\mathrm {K} (\alpha , \ulcorner \forall x \in \mathrm {Ag} \hspace {2pt} \big ( A(x) \rightarrow \mathrm {K}(\alpha , \ulcorner \mathrm {CK}_A(\ulcorner \phi \urcorner ) \urcorner ) \urcorner )$ . Third, applying deductive closure to the latter, … Continuing in this way, we obtain the infinite sequence of belief assertions characteristic of common belief: Every agent satisfying A believes $\phi $ , and believes “every agent satisfying A believes $\phi $ ”, and so on. A merit of the present formalization is that it goes one step further than this sequence, as it also entails that every agent satisfying A believes “the agents satisfying A have common belief of $\phi $ ”. Moreover, note that by the $\leftarrow $ direction of ( $\mathsf {CBE}$ ), $\mathrm {CK}_A$ is the weakest formula entailing the above assertions.

The results in this section are related to results on self-reference due to Smoryński [19, chap. 4]. They are proved by the same technique, using Löb’s theorem from [16]

Theorem 2 (Löb).

Let S be a (recursively enumerable) system extending $\mathsf {PA}$ , and let $\phi $ be a sentence in its language. If $S \vdash \Pr _S(\ulcorner \phi \urcorner ) \rightarrow \phi $ , then $S \vdash \phi $ .

Lemma 3. Let $A(x), \theta (y), \theta '(y)$ be $\mathcal {L}$ -formulas such that

Then

Proof. We start by showing that $\mathsf {DCB}$ proves

(†)

By , and universal instantiation internal to ${\Pr }_{\mathsf {DCB} }$ ,

Distributing the substitution, and applying $\mathsf {R}_{\mathsf {DCB}} $ to this, we obtain

Now by $\textsf {UK}^{\mathrm {K}}$ ,

It follows from this, and the definition of $\Psi _A$ , that

establishing ().

By () and the assumption of this theorem,

So by Löb’s theorem,

as desired.

From the above result we obtain uniqueness of the defined common belief predicate, with respect to provability in $\mathsf {DCB.} $

Corollary 4 (Uniqueness of defined common belief).

Let $\mathrm {CK}^{\prime }_A(y)$ be an $\mathcal {L}$ -formula such that

Then

Proof. Since

the result follows by applying Lemma 3 in both directions.

The philosophical upshot is that if we require generally of defined common belief predicates that our theory of syntax $\mathsf {Base}$ (or even $\mathsf {DCB}$ ) is sufficient to prove that they are adequate representations of common belief (in the sense that they satisfy the common belief equivalence), then they are unique up to equivalence in $\mathsf {DCB}$ .

I will now use these results to relate the internally quantified iterative definition of common belief to my fixed point definition:

Iteratively, for $n < \omega $ , the $\mathcal {L}$ -formula $\mathrm {ICK}^n_A(y)$ (n-Iterated Common Belief) with only y free, is defined as follows:

By a simple induction argument, for all $n \leq m < \omega $ , we have .

Now by McGee’s trick from [17], there is a formula $\mathrm {ICK}_A(y)$ , which is intuitively the (internal) infinite conjunction of all these formulas. In brief, the iterative definition above can be represented by a function f defined in $\mathcal {L}$ , such that $\mathsf {Base} \vdash \forall n \hspace {2pt} \big (f(n) = \ulcorner \mathrm {ICK}^n_A \urcorner \big )$ . Then $\mathrm {ICK}_A(y)$ can be defined as follows:

Note that for all $n < \omega $ , we have .

The following theorem elucidates the relationship between the formalizations $\mathrm {CK}$ and $\mathrm {ICK}$ of common belief.

Theorem 5.

1. (a)

2. (b)

Proof. Let .

1. (a) By Lemma 3, it suffices to show in $\mathsf {DCB}$ that

   

   Assume . Trivially, we obtain $\mathrm {ICK}^0_A(u)$ . Let $x \in \mathrm {Ag}$ and let $n < \omega $ . We need to establish . By and the deductive closure properties of $\mathsf {DCB}$ , this follows from the assumption.

2. (b) By the proof of (a) and Corollary 4, it suffices to show in $\mathsf {DCB}$ that

   

   Assume

   (Assumption)

   
   and let $x \in \mathrm {Ag}$ . We obtain $\mathrm {K}(x, u)$ from $\mathrm {ICK}^0_A(u)$ , and we obtain by the case $n = 0$ of the assumption. So by the deductive closure properties of $\mathsf {DCB}$ , to establish , we need to show that
   

   The formal details of nested substitution start to conflict with readability here, so we proceed semi-formally. By $\mathsf {UBF}$ , the quantifier “ $\forall n' < \omega $ ” can be moved out of “ $\mathrm {K}\Big [x, \cdots \Big ]$ ”. It becomes in front of it, and t is substituted for $n'$ in the second argument of “ $\mathrm {K}\Big [x, \cdots \Big ]$ ”. Thus, let . By the deductive closure properties, we have , for some $n < \omega $ , and it suffices to show that

   

   Now note that the latter is implied by , which in turn follows from (Assumption).

Here is another useful application of Corollary 4.

Lemma 6. Let $A(x) \in \mathcal {L}$ and let $\phi , \psi \in \mathcal {L}^0$ .

$$ \begin{align*} \mathsf{DCB} \vdash \mathrm{CK}_A(\ulcorner \phi \urcorner) \wedge \mathrm{CK}_A(\ulcorner \psi \urcorner) \leftrightarrow \mathrm{CK}_A(\ulcorner \phi \wedge \psi \urcorner). \end{align*} $$

Proof. Let $\theta $ be the formula $\mathrm {CK}_A(\ulcorner \phi \urcorner ) \wedge \mathrm {CK}_A(\ulcorner \psi \urcorner )$ . We work in $\mathsf {DCB} $ . By Corollary 4, it suffices to show that

$$ \begin{align*} \theta \leftrightarrow \Psi_A(\ulcorner \phi \wedge \psi \urcorner, \ulcorner \theta \urcorner). \end{align*} $$

This is shown by the following equivalences:

$$ \begin{align*} & \mathrm{CK}_A(\ulcorner \phi \urcorner) \wedge \mathrm{CK}_A(\ulcorner \psi \urcorner) \\ \iff {} & \forall x \hspace{2pt} \Big(A(x) \rightarrow \big[ \mathrm{K}(x, \ulcorner \phi \urcorner) \wedge \mathrm{K}(x, \ulcorner \psi \urcorner) \wedge \mathrm{K} \big( x, \ulcorner \mathrm{CK}_A(\ulcorner \phi \urcorner) \urcorner \big)\\&\qquad\qquad\quad\wedge \mathrm{K} \big( x, \ulcorner \mathrm{CK}_A(\ulcorner \psi \urcorner) \urcorner \big) \big] \Big) \\ \iff {} & \forall x \hspace{2pt} \Big(A(x) \rightarrow \big[ \mathrm{K}(x, \ulcorner \phi \wedge \psi \urcorner) \wedge \mathrm{K} \big( x, \ulcorner \mathrm{CK}_A(\ulcorner \phi \urcorner) \wedge \mathrm{CK}_A(\ulcorner \psi \urcorner) \urcorner \big) \big] \Big). \end{align*} $$

The last equivalence follows from $\textsf {UK}^{\mathrm {K}}$ and $\mathsf {NEC}^{\mathrm {K}}$ .

Lemma 3 can be generalized as follows.

Lemma 7. Suppose that $A(x), B(x), \theta (y), \theta '(y)$ are $\mathcal {L}$ -formulas and f is a function definable in $\mathsf {DCB} $ , such that $\mathsf {DCB} $ proves

Then

Proof. It suffices to indicate how the proof of Lemma 3 is amended. The key difference is that now we need to show that $\mathsf {DCB} $ proves

(‡)

Just as before, we prove from that

From this and the new assumptions it follows that

establishing ().

Corollary 8. Suppose that $A(x), B(x)$ are $\mathcal {L}$ -formulas and f is a function definable in $\mathsf {DCB} $ , such that $\mathsf {DCB} $ proves

Then

Proof. A direct application of Lemma 7 with $\mathrm {CK}_A$ as $\theta $ and $\mathrm {CK}_B$ as $\theta '$ .

The following theorem shows that the deductive closure properties axiomatized for $\mathrm {K}$ in $\mathsf {DCB}$ carry over to each common belief predicate $\mathrm {CK}_A$ , without the need for any primitive predicate or axiom for $\mathrm {CK}_A.$

Theorem 9 (Deductive closure of common belief).

Let $A(x) \in \mathcal {L}$ .

1. (a)

2. (b)

3. (c) For each $\phi \in \mathcal {L}^0$ : $\mathsf {DCB} \vdash \phi \phantom {~~} \Longrightarrow \phantom {~~} \mathsf {DCB} \vdash \mathrm {CK}_A(\ulcorner \phi \urcorner ).$

Proof.

1. (a) $\mathsf {DCB} $ defines a function f such that

   

   Moreover,

   

   So by Corollary 8,

   

   By Lemma 6,

   
   whence the result follows.

2. (b) By Lemma 3, with $\Pr _{\mathsf {DCB}}$ as $\theta $ and with $\mathrm {CK}_A$ as $\theta '$ , it suffices to show that

   

   By $\mathsf {R}_{\mathsf {DCB}} $ ,

   

   It is a well-known property of provability that

   

   So by $\mathsf {R}_{\mathsf {DCB}} $ ,

   

   Combining the second and fourth displayed item, we obtain the first displayed item, as desired.

3. (c) Assume that $\mathsf {DCB} \vdash \phi $ . Since $\Pr _{\mathsf {DCB}}$ represents provability in $\mathsf {DCB}$ , we have $\mathsf {Base} \vdash \Pr _{\mathsf {DCB}}(\ulcorner \phi \urcorner )$ . Hence, $\mathsf {DCB} \vdash \mathrm {CK}_A(\ulcorner \phi \urcorner )$ , by the previous item of this theorem.

4 Extension to a system of knowledge with a revision semantics

This section extends $\mathsf {DCB}$ to the system $\mathsf {KT}$ (of Knowledge and Truth, axiomatized in Figure 3), and shows that it has a natural revision semantics. $\mathsf {KT}$ utilizes both the predicate symbol $\mathrm {K}$ , formalizing knowledge, and $\mathrm {T}$ , formalizing truth. The revision semantics was introduced independently by Gupta and Herzberger in [7], [11] and [12], as an approach to resolve the liar paradox. $\mathsf {FS}$ (the Friedman–Sheard system of truth, axiomatized in Figure 2), which is also a subsystem of $\mathsf {KT}$ , was introduced in [5]. Its present axiomatization, and its formal revision semantics were established in [9]. A self-contained exposition of central results concerning $\mathsf {FS}$ is found in [10, chap. 14].

Figure 2 Axioms and rules of $\mathsf {FS.} $

Figure 3 Axioms and rules of $\mathsf {KT.} $

The bulk of this section is devoted to explaining a straight-forward generalization of Stern’s revision semantics from [20] to multi-agent knowledge. However, it also contains key original technical results, encapsulated in Lemmata 14 and 13, which show that $\mathsf {DCB}$ can be validated in this semantics. From these results the penultimate Theorem 15 is obtained, which establishes that all of $\mathsf {KT} + \mathsf {UBF} + \mathsf {IA} + \mathsf {In}^+ + \mathsf {In}^-$ (see Figure 4) can be validated in this semantics.

Figure 4 Supplementary axioms.

The basic idea of the revision semantics is to start with a ground model $\langle \mathcal {M}, P_0 \rangle $ (where $P_0$ is an interpretation of the truth predicate), and iteratively revise the interpretation of the truth predicate to $P_1, P_2, \cdots $ , by the recursion $P_{n+1} =_{\mathrm {df}} \big \{ \mathrm {gc}(\sigma ) \mid \langle \mathcal {M}, P_n \rangle \models \sigma \big \}$ . The map defined by $P \mapsto \big \{ \mathrm {gc}(\sigma ) \mid \langle \mathcal {M}, P \rangle \models \sigma \big \}$ , for all $P \subseteq \mathbb {N}$ , is called the revision semantic operator.

It follows from McGee’s theorem [17], that $\mathsf {FS}$ is $\omega $ -inconsistent. In particular, it has no standard model. However, the intimate connection between $\mathsf {FS}$ and the revision semantics vindicates $\mathsf {FS}$ : Take the standard model of arithmetic expanded with an arbitrary interpretation of the truth predicate as the ground model; call it $\langle \mathbb {N}, P_0 \rangle $ . In [9], Halbach showed that $\mathsf {FS}$ is locally validated in the revision semantics, meaning that for each finite fragment of $\mathsf {FS} $ , there is $n \in \mathbb {N}$ , such that for all $m \geq n$ , $\langle \mathbb {N}, P_m \rangle $ is a standard model of that fragment. Since every proof only uses finitely many axioms, one only needs a finite fragment for any particular deductive application of the system. Hence, for any application of $\mathsf {FS}$ , an adequate standard model can be obtained by a finite iteration of the revision semantic operator. Theorem 15 establishes the analogous local validation property for $\mathsf {KT} + \mathsf {UBF} + \mathsf {IA} + \mathsf {In}^+ + \mathsf {In}^-$ .

In [20], Stern showed that necessitation and truth (treated as predicates) can be formalized in a range of systems extending $\mathsf {FS}$ , and provided a flexible generalized revision semantics locally validating them. Since $\mathsf {KT}$ axiomatizes knowledge for multiple agents, I have generalized this semantics slightly. It builds on a conventional possible worlds semantics; each world is a standard $\mathcal {L}_-$ -structure satisfying $\mathsf {Base}$ , and each agent is associated with a binary accessibility relation on the set of worlds. It involves evaluation functions, which map each world to the set of Gödel codes of true sentences in that world. Any evaluation function induces interpretations of $\mathrm {K}$ and $\mathrm {T}$ in each world, expanding each world to an $\mathcal {L}$ -structure. The revision semantic operator maps each evaluation function to a revised evaluation function, thus inducing a revised $\mathcal {L}$ -expansion of each world.

The results of [20] are developed in a setting where the base system is $\mathsf {PA}$ extended with induction for the language obtained by augmenting $\mathcal {L}_{\mathsf {PA}}$ with the predicates $\mathrm {N}$ and $\mathrm {T}$ . [20] also provides an explanation for how to generalize to other base systems, which applies to $\mathsf {PA}(\mathcal {L})$ . I assume that $\mathsf {Base} = \mathsf {PA}(\mathcal {L})$ throughout this section.

I proceed to go through the generalized definitions and theorems that are relevant for this paper. All worlds are assumed to be standard expansions of the standard model $\mathbb {N}$ and, for simplicity, it is assumed that the interpretation of $\mathrm {Ag}$ is identical in all worlds. It is straight-forward to generalize to diverse interpretations of $\mathrm {Ag}$ . Fix a non-empty subset $G \subseteq \mathbb {N}$ , whose elements are called agents. For any first-order language L expanding $\mathcal {L}_{\mathsf {PA}}$ , an L-agency-frame for G is a tuple $F = \langle W, (R_\alpha )_{\alpha \in G} \rangle $ , where W is a set of L-expansions of $\mathbb {N}$ interpreting $\mathrm {Ag}$ by G, and $R_\alpha $ is a binary relation on W, for each $\alpha \in G$ .

For the rest of this section, fix an $\mathcal {L}_-$ -agency-frame F for G. For each agent $\alpha \in G$ : $\langle W, R_\alpha \rangle $ is called the $\mathcal {L}_-$ -Kripke-frame of $\alpha $ , the elements of W are called worlds, and $R_\alpha $ is called the accessibility relation of $\alpha $ . An evaluation function of F is a function $f : W \rightarrow \mathcal {P}(\mathbb {N})$ , thought of as mapping a world to the set of Gödel codes of true sentences in that world. $\mathrm {Val}_F$ denotes the set of all evaluation functions of F. For the rest of this paragraph, fix $f \in \mathrm {Val}_F$ . $f_\alpha : W \rightarrow \mathcal {P}(\mathbb {N})$ and $f^{\mathrm {K}} : W \rightarrow \mathcal {P}(\mathbb {N} \times \mathbb {N})$ are defined as follows, for all $\alpha \in G$ and all $w \in W$ :

$$ \begin{align*} f_\alpha(w) &=_{\mathrm{df}} \bigcap \{ f(v) \mid w R_\alpha v \} \\ f^{\mathrm{K}}(w) &=_{\mathrm{df}} \{ \langle \alpha, \phi \rangle \mid \alpha \in G \wedge \phi \in f_\alpha(w) \}. \end{align*} $$

For each $\mathcal {L}_-$ -model $w \in W$ , f induces an $\mathcal {L}$ -expansion $w^f$ of w, in which $\mathrm {T}$ is interpreted by $f(w)$ , $\mathrm {K}^2$ is interpreted by $f^{\mathrm {K}}(w)$ , and $\mathrm {K}^1$ is interpreted by $\big \{\phi \mid \forall \alpha \in G \hspace {2pt} (\langle \alpha , \phi \rangle \in f^{\mathrm {K}}(w))\big \}$ . Thus, f also induces an $\mathcal {L}$ -agency-frame $F^f =_{\mathrm {df}} \big \langle W^f, (R^f_\alpha )_{\alpha \in G} \big \rangle $ , where $W^f =_{\mathrm {df}} \big \{w^f \mid w \in W\big \}$ and $R^f_\alpha =_{\mathrm {df}} \big \{ \big \langle v^f, w^f \big \rangle \mid \big \langle v, w \big \rangle \in R_\alpha \big \}$ , for each $\alpha \in G$ .

The revision semantic operator, $\Gamma : \mathrm {Val}_F \rightarrow \mathrm {Val}_F$ , is defined as follows, for all $f \in \mathrm {Val}$ and all $w \in W$ :

$$ \begin{align*} \big(\Gamma(f)\big)(w) =_{\mathrm{df}} \big\{ \mathrm{gc}(\phi) \mid w^f \models \phi \big\}. \end{align*} $$

Note that for any $\mathcal {L}$ -agency-frame of the form $F^f$ (where F is an $\mathcal {L}_-$ -agency-frame and $f \in \mathrm {Val}_F$ ), $\Gamma $ induces a revised $\mathcal {L}$ -agency-frame $F^{\Gamma (f)}$ . This revision is iterated by iterated applications of $\Gamma $ , providing a revision semantics appropriate for the setting of this paper. This revision semantics is closely related to the system $\mathsf {BEFS}$ (Basic Epistemic Friedman–Sheard), axiomatized in Figure 5. ⁴

Figure 5 Axioms and rules of $\mathsf {BEFS.}$

The axiom $\mathsf {UNS}^{\mathrm {K}}$ (Untyped Necessitated Substitution principle) of $\mathsf {BEFS}$ asserts that knowledge is preserved under substitution of $\mathcal {L}_{\mathsf {PA}}$ -terms that evaluate to the same value. The axiom $\mathsf {UND}^{\mathrm {K}}$ (Untyped Necessity of Distinctness) of $\mathsf {BEFS}$ asserts that it is known whenever two $\mathcal {L}_{\mathsf {PA}}$ -terms evaluate to distinct values (the analog for equality is provable in the system).

Proposition 10. $\mathsf {KT} + \mathsf {UBF} + \mathsf {IA} \equiv \mathsf {BEFS} + \mathsf {V} + \mathsf {R}_{\mathsf {DCB}}$ .

Proof. By $\mathsf {CONEC}^{\mathrm {T}}$ and $\mathsf {NEC}^{\mathrm {K}}$ , $\mathsf {KT} + \mathsf {UBF} + \mathsf {IA}$ admits the rule $\mathrm {T}/\mathrm {K}$ . By $\mathsf {NEC}^{\mathrm {T}}$ and $\mathrm {T}/\mathrm {K}$ , $\mathsf {BEFS} + \mathsf {V} + \mathsf {R}_{\mathsf {DCB}}$ admits $\mathsf {NEC}^{\mathrm {K}}$ . It remains only to prove $\mathsf {UNS}^{\mathrm {K}}$ and $\mathsf {UND}^{\mathrm {K}}$ in $\mathsf {KT}$ . Since evaluation of $\mathcal {L}_{\mathsf {PA}}$ -terms is primitive recursive, $\mathsf {PA}$ proves that the antecedent $s^\circ = t^\circ $ of $\mathsf {UNS}^{\mathrm {K}}$ is equivalent to . Therefore, it is straight-forward to prove $\mathsf {UNS}^{\mathrm {K}}$ from $\mathsf {R}_{\mathsf {DCB}}$ , $\mathsf {UK}^{\mathrm {K}}$ and $\mathsf {NEC}^{\mathrm {K}}$ . The same method also works for $s^\circ \neq t^\circ $ , establishing $\mathsf {UND}^{\mathrm {K}}$ analogously.

One might feel that the untyped version of axiom $\mathsf {4}$ from modal logic,

(U4)

is a straight-forward formalization of the positive introspection principle, but as established by the following proposition, it is inconsistent with $\mathsf {KT}$ . It turns out that $\mathsf {In}^+$ is the appropriate formalization of positive introspection in this genuinely untyped setting.

Proposition 11. $\mathsf {KT} + \mathsf {U4}$ is inconsistent.

Proof. Consider , such that . Assume . Then we obtain from $\mathsf {U4}$ . But , so by basic deductive closure (following from $\mathsf {NEC}^{\mathrm {K}}$ and $\mathsf {UK}^{\mathrm {K}}$ ), we obtain and $\mathrm {K}(\bot )$ . Now by $\mathsf {V}$ , we have $\mathrm {T}(\bot )$ , from which $\bot $ is obtained by the axiom $\mathsf {UCT}^{\mathrm {Atom}}$ of $\mathsf {FS}$ . This proves , which is equivalent to . Having proved , we obtain by $\mathsf {NEC}^{\mathrm {K}}$ , which is equivalent to , a contradiction.

A pseudo-system is defined as a recursively enumerable set of sentences in a first-order language. Pseudo-systems constitute an auxiliary tool for approximating systems. For each $2 \leq n < \omega $ , the pseudo-systems $\mathsf {BEFS}_n$ and $\mathsf {EFS}_n$ are defined as $\mathsf {BEFS}$ and $\mathsf {EFS}$ , respectively, except that at most a total of $n - 1$ applications of $\mathsf {NEC}^{\mathrm {T}}$ and $\mathsf {CONEC}^{\mathrm {T}}$ are allowed in a proof. The systems $\mathsf {BEFS}_0$ and $\mathsf {EFS}_0$ are defined as $\mathsf {PA}(\mathcal {L})$ . The systems $\mathsf {BEFS}_1$ and $\mathsf {EFS}_1$ are given by the axioms of $\mathsf {BEFS}$ and $\mathsf {EFS}$ , respectively, in addition to the axiom $\mathsf {R}_{\mathsf {PA}(\mathcal {L})}^{\mathrm {T}}$ below, and the deductive rule $\mathrm {T} / \mathrm {K}$ .

(R _PA(L) ^T) $$\begin{align} \forall \phi \in \mathcal{L}^0 \hspace{2pt} \big( {\Pr}_{\mathsf{PA}(\mathcal{L})}(\phi) \rightarrow \mathrm{T}(\phi) \big). \end{align} $$

For any function $h : A \rightarrow B$ and any $A' \subseteq A$ , $h[A'] =_{\mathrm {df}} \{h(a) \mid a \in A'\}$ . Let $R \subseteq A \times A$ . R is Euclidean if $\forall a, b, c \in A \hspace {2pt} \big ( (aRb \wedge aRc) \rightarrow bRc \big )$ .

Theorem 12. Let $f \in \mathrm {Val}_F$ and let $n < \omega $ .

1. (a) Then

   $$ \begin{align*} f \in \Gamma^n[\mathrm{Val}_F] &\Longleftrightarrow \forall w \in W \hspace{2pt} \big( w^f \models \mathsf{BEFS}_n \big). \end{align*} $$

2. (b) If $R_\alpha $ is reflexive and $1 \leq n$ , then

   $$ \begin{align*} f \in \Gamma^n[\mathrm{Val}_F] &\Longleftrightarrow \forall w \in W \hspace{2pt} \big( w^f \models \mathsf{BEFS}_n + \mathsf{V} \big). \end{align*} $$

3. (c) If $R_\alpha $ is transitive and $1 \leq n$ , then

   $$ \begin{align*} f \in \Gamma^n[\mathrm{Val}_F] &\Longleftrightarrow \forall w \in W \hspace{2pt} \big( w^f \models \mathsf{BEFS}_n + \mathsf{In}^+ \big). \end{align*} $$

4. (d) If $R_\alpha $ is Euclidean and $1 \leq n$ , then

   $$ \begin{align*} f \in \Gamma^n[\mathrm{Val}_F] &\Longleftrightarrow \forall w \in W \hspace{2pt} \big( w^f \models \mathsf{BEFS}_n + \mathsf{In}^- \big). \end{align*} $$

Proof. I explain how to generalize the proofs of Theorems 4.11 and 4.12 in [20] to the multi-agent setting. First note that the axioms and rules of $BMFS$ from [20] are directly generalized to corresponding multi-agent axioms of $\mathsf {BEFS}$ . Moreover, $\mathsf {V}$ is the direct generalization of $T'$ from [20] to the multi-agent setting. Using $\mathsf {IA}$ and $\mathsf {UCT}^\neg $ , it is seen that the axioms $\mathsf {In}^+$ and $\mathsf {In}^-$ are equivalent to the direct generalizations of $4'$ and $E'$ in [20] to the multi-agent setting, respectively.

$\textsf {Non-triviality}$ follows from that G is non-empty. $\mathrm {K}^1$ - $\mathrm {K}^2$ follows from the interpretation of $\mathrm {K}^1$ in the definition of $w^f$ (for any $w \in W$ ). The other axioms concerned are all universally quantified over $\mathrm {Ag}$ . We generalize from Stern’s single unary necessity predicate $\mathrm {N}$ to a countable set $\{\mathrm {K}_\alpha \mid \alpha \in G\}$ of unary knowledge predicates (one for each agent). Note that for a standard model, interpretations of $\mathrm {Ag}$ and the binary knowledge predicate $\mathrm {K}$ induce a set G of agents and an interpretation of $\mathrm {K}_\alpha $ for each $\alpha \in G$ ; and vice versa. Letting $\alpha \in G$ be arbitrary, the verification of the axioms then proceeds exactly as in [20], for the single unary predicate $\mathrm {K}_\alpha $ and the single accessibility relation $R_\alpha $ .

The left-to-right directions of the above theorem show that for any finite fragment of $\mathsf {BEFS} + \mathsf {V} + \mathsf {In}^+ + \mathsf {In}^-$ , it is satisfied by all the worlds in the $\mathcal {L}$ -agency-frame induced by an evaluation function of F obtained by a finite number of revisions of an arbitrary evaluation function of F. The following lemmata are provided for the sake of extending this result to the axiom $\mathsf {R}_{\mathsf {DCB}}$ .

Let $R \subseteq A \times A$ . R is left-total if for each $a \in A$ there is $b \in A$ , such that $a R b$ . Note that if R is reflexive, then it is left-total.

Lemma 13. If for all $\alpha \in G$ , $R_\alpha $ is left-total, and f is an evaluation function, such that for all $w \in W$ , there is an $\mathcal {L}$ -system $S_w$ extending $\mathsf {DCB}$ , such that $f(w) = \big \{ \mathrm {gc}(\sigma ) \mid S_w \vdash \sigma \big \}$ , then for all $w \in W$ , $w^f \models \mathsf {DCB}$ .

Proof. Let $w \in W$ be arbitrary. Since the theorems of $S_w$ are closed under modus ponens and $R_\alpha $ is left-total for all $\alpha \in G$ , we have that $w^f \models \mathsf {UK}^{\mathrm {K}}$ . Since w is standard, we have for all $\sigma \in \mathcal {L}^0$ that $S_w \vdash \sigma \iff w \models \Pr _{S_w}(\ulcorner \sigma \urcorner )$ . So since $S_w \vdash \mathsf {DCB}$ , $f(w) = \big \{ \mathrm {gc}(\sigma ) \mid S_w \vdash \sigma \big \}$ , and $R_\alpha $ is left-total for all $\alpha \in G$ , we have that $w^f \models \mathsf {R}_{\mathsf {DCB}}$ .

Lemma 14. Let $f \in \mathrm {Val}_F$ , and assume that for all $\alpha \in G$ , $R_\alpha $ is left-total, and that for all $w \in W$ , $w^f \models \mathsf {DCB}$ . Then for all $n < \omega $ , and for all $w \in W$ , $w^{\Gamma ^n(f)} \models \mathsf {DCB}$ .

Proof. We prove this by induction. Let $w \in W$ be arbitrary. By assumption, $w^f \models \mathsf {DCB}$ . Suppose that $w^{\Gamma ^n(f)} \models \mathsf {DCB}$ , for some $n < \omega $ . Then $\big \{ \mathrm {gc}(\sigma ) \mid \mathsf {DCB} \vdash \sigma \big \} \subseteq \big (\Gamma ^{n+1}(f)\big )(w)$ . Thus, for each $\alpha \in G$ , it follows from left-totality of $R_\alpha $ that $\big \{ \big \langle \alpha , \mathrm {gc}(\sigma ) \big \rangle \mid \mathsf {DCB} \vdash \sigma \big \} \subseteq \big (\Gamma ^{n+1}(f)\big )^{\mathrm {K}}(w)$ . Moreover, since w is standard, we have for all $\sigma \in \mathcal {L}^0$ that $\mathsf {DCB} \vdash \sigma \iff w \models \Pr _{\mathsf {DCB}}(\ulcorner \sigma \urcorner )$ . Combining these facts, we get that $w^{\Gamma ^{n+1}(f)} \models \mathsf {R}_{\mathsf {DCB}}$ . Moreover, it follows from Theorem 12 that for all $k \geq 1$ , $w^{\Gamma ^k(f)} \models \mathrm {K}^1\text {-}\mathrm {K}^2 + \mathsf {UK}^{\mathrm {K}}$ . So $w^{\Gamma ^{n+1}(f)} \models \mathsf {DCB}$ , as desired.

Theorem 15. Let f be an evaluation function, such that for all $w \in W$ , there is an $\mathcal {L}$ -system $S_w \vdash \mathsf {DCB}$ , such that $f(w) = \big \{ \mathrm {gc}(\sigma ) \mid S_w \vdash \sigma \big \}$ .

1. (a) For each finite $\Phi \subseteq \mathsf {DCB} + \mathsf {FS} + \mathsf {UBF} + \mathsf {IA}$ , there is $m < \omega $ , such that for all $n \geq m$ and all $w \in W$ ,

   $$ \begin{align*} w^{\Gamma^n(f)} \models \Phi. \end{align*} $$

2. (b) If $R_\alpha $ is reflexive for all $\alpha \in G$ , then for each finite $\Phi \subseteq \mathsf {KT} + \mathsf {UBF} + \mathsf {IA}$ , there is $m < \omega $ , such that for all $n \geq m$ and all $w \in W$ ,

   $$ \begin{align*} w^{\Gamma^n(f)} \models \Phi. \end{align*} $$

3. (c) If $R_\alpha $ is reflexive and transitive for all $\alpha \in G$ , then for each finite $\Phi \subseteq \mathsf {KT} + \mathsf {UBF} + \mathsf {IA} + \mathsf {In}^+$ , there is $m < \omega $ , such that for all $n \geq m$ and all $w \in W$ ,

   $$ \begin{align*} w^{\Gamma^n(f)} \models \Phi. \end{align*} $$

4. (d) If $R_\alpha $ is reflexive, transitive and Euclidean for all $\alpha \in G$ , then for each finite $\Phi \subseteq \mathsf {KT} + \mathsf {UBF} + \mathsf {IA} + \mathsf {In}^+ + \mathsf {In}^-$ , there is $m < \omega $ , such that for all $n \geq m$ and all $w \in W$ ,

   $$ \begin{align*} w^{\Gamma^n(f)} \models \Phi. \end{align*} $$

Proof. This result is immediate from combining Theorem 12, Lemmata 13 and 14.

Corollary 16. $\mathsf {KT} + \mathsf {UBF} + \mathsf {IA} + \mathsf {In}^+ + \mathsf {In}^-$ is consistent.

Proof. This follows from Theorem 15 and the soundness of first-order logic.

5 Concluding discussion

In §3, it was shown that the simple doxastic system $\mathsf {DCB}$ defines common belief, and that it proves that common belief has desirable uniqueness and deductive closure properties. The combination of that $\mathsf {DCB}$ has simple and well-motivated axioms, and that it has this deductive power, yields that $\mathsf {DCB}$ provides explanatory philosophical insight on common belief. In §4 it was further shown that $\mathsf {DCB}$ can be extended to a comprehensive system of knowledge and truth with a natural revision semantics, which is axiomatized as $\mathsf {KT} + \mathsf {UBF} + \mathsf {IA}$ along with supplementary introspection axioms that its user may want to include. This system is a viable option for overcoming the knower paradoxes of [14] and [18]. I find it compelling because of the significant features it has, listed in §1. Here follow comments on these features, as well as a discussion on the axiom $\mathsf {IA}$ , and a summary of further significant features inherited from $\mathsf {FS}$ .

1. 1. First-order: The predicate approach is more general than the operator approach. In particular, as pointed out in §4, the revision semantics generalizes Hintikka’s possible worlds semantics for epistemic logic pioneered in [13]. This added generality manifests in a variety of ways, including the following:

   1. (a) Being based on the conventional foundation of mathematics (i.e., $\mathsf {PA}$ or $\mathsf {ZFC}$ ), the predicate approach allows seamless integration of any scientific results expressible in a formal theory that can be implemented in conventional mathematics.

   2. (b) The predicate approach accommodates sentences like in Montague’s paradox, which is not possible in the operator approach because of monotonicity constraints on the fixed point constructor.

   3. (c) The predicate approach accommodates certain epistemically relevant principles, such as $\mathsf {UBF}$ , that cannot be expressed in a pure operator approach.

   4. (d) It is straight-forward to generalize the knowledge predicate to a three-place relation, where the new argument is intended to hold a representation for a justification of the knowledge assertion in question. This is significant for developing a more nuanced formal epistemology. For example, it enables a formalization of Clark’s solution [2] to Gettier’s problem [6].

2. 2. Faithful formalizations: $\mathsf {KT}$ formalizes the principle of veracity more faithfully than how it is formalized in the knower paradoxes, by utilizing both a knowledge and a truth predicate. Since $\textsf {R}_{\mathsf {DCB}}$ entails the schema $\mathsf {I}^{\mathrm {K}}$ assumed in the paradox of Kaplan and Montague, $\mathsf {UT}^{\mathrm {K}}$ and $\mathrm {K}[\mathsf {UT}^{\mathrm {K}}]$ are the only axiom schemata of the knower paradoxes that are not provable in $\mathsf {KT}$ . Still, the corresponding sentences $\mathsf {V}$ and $\mathrm {K}(\ulcorner \mathsf {V} \urcorner )$ , respectively, are provable, thus preserving the corresponding epistemic principles.

3. 3. Deductive closure: $\mathsf {KT}$ has the rule $\mathsf {NEC}^{\mathrm {K}}$ , formalizing the natural assumption that ones axioms are known and that deductive reasoning from these axioms is a legitimate method for generating knowledge. ⁵ For example, it proves a schema expressing that all agents have sufficient knowledge about the syntax, e.g., that they all know “ $\ulcorner \phi \wedge \psi \urcorner $ is the conjunction of $\ulcorner \phi \urcorner $ and $\ulcorner \psi \urcorner $ ”. The axiom $\mathsf {UK}^{\mathrm {K}}$ of $\mathsf {KT}$ asserts that knowledge is closed under modus ponens. Together, $\mathsf {NEC}^{\mathrm {K}}$ and $\mathsf {UK}^{\mathrm {K}}$ ensure that for any $\phi , \psi \in \mathcal {L}$ , if $\mathsf {KT} \vdash \mathrm {K}(\ulcorner \phi \urcorner )$ and $\mathsf {KT} \vdash \phi \rightarrow \psi $ , then $\mathsf {KT} \vdash \mathrm {K}(\ulcorner \psi \urcorner )$ . So in this sense, $\mathsf {KT}$ formalizes the intuition that knowledge is closed under any (as externally quantified) reasoning sanctioned by $\mathsf {KT}$ . Moreover, by $\mathsf {R}_{\mathsf {DCB}}$ it also proves deductive closure for all (internally quantified) reasoning in $\mathsf {DCB}$ . The precise formulation of $\mathsf {R}_{\mathsf {DCB}}$ is also instrumental to the proofs in §3, establishing analogous deductive closure properties of common belief/knowledge.

4. 4. Genuinely untyped: A common approach to curb the role self-reference plays in the paradoxes, while allowing self-reference in the language, is to introduce a typing-regiment. One may e.g., introduce a hierarchy of symbols $\mathrm {K}_i$ , for all $i < \omega $ , and formulate the axioms about each $\mathrm {K}_i$ so that they only apply to formulas not including $\mathrm {K}_j$ for all $j \geq i$ . Anderson’s [1] is a prominent example of this approach to addressing the knower paradox of [14]. However, this is hard to motivate philosophically and it cripples reasoning with useful self-referential formulas such as defined common knowledge predicates. In contrast, $\mathsf {KT}$ is designed to be genuinely untyped. This is achieved in that it only has one knowledge and one truth predicate, and, importantly, that all relevant axioms quantify universally over the whole language (or ). Moreover, the untyped approach is explicitly utilized in that it allows the self-referential axiom $\mathsf {R}_{\mathsf {DCB}}$ .

5. 5. Explanation of common knowledge:

   1. (a) $\mathsf {KT}$ only formalizes epistemic principles for reasoning about the knowledge of individual agents. Nonetheless, it defines common knowledge and proves that common knowledge satisfies analogous principles. These explanatory advantages stem from the desirable properties of $\mathsf {DCB}$ , and in particular of $\mathsf {R}_{\mathsf {DCB}}$ , in relation to common knowledge and the revision semantics, established in §3 and §4, respectively.

   2. (b) Formalizations of common knowledge have previously been developed within the modal operator approach to epistemic logic. This can either be done by introducing a primitive common knowledge operator for each collection of agents (as in [4, chap. 2.4]) along with axioms formalizing these as common knowledge, or by introducing a greatest fixed point constructor and modifying the semantics to accommodate this advanced syntactic device (as in [4, chap. 11.5]). Here follow comparisons between these operator approaches and the present predicate approach:

      1. i. As we have seen, the present predicate approach allows for common knowledge to be defined as a fixed point in terms of individual knowledge, and it explains the deductive closure of common knowledge from the deductive closure of individual knowledge. The operator approaches require the introduction of additional logical machinery, either primitive common knowledge operators and additional axioms, or a more general fixed point constructor and an extended semantics to accommodate it. Thus, the present predicate approach is arguably more successful in explaining common knowledge directly in terms of individual knowledge.

      2. ii. As explained above, the predicate approach naturally generalizes to formalize the justification an agent has for their knowledge. This is also significant for common knowledge: in many natural situations, when an agent knows that another agent knows something, then the former also knows the latter’s justification for this, which counts as a justification for the former as well. So in many natural situations, common knowledge entails some notion of “common justification”. ⁶ As the predicate approach provides a convenient avenue to formalize this intuitive notion, it enables further research clarifying this matter.

      3. iii. In the operator approaches, it follows from the possible worlds semantics that the fixed point definition of common knowledge is equivalent to the definition as an infinite conjunction of iterated knowledge assertions (see [4, chap. 11.5.2]). Analogously, the revision semantics of §4 also validates this equivalence: Indeed, Theorem 15 shows that $\mathsf {UBF}$ is validated in this revision semantics, so by Theorem 5, we have the equivalence. Thus, in the full approach of this paper, the two definitions of common knowledge also coincide.

         On the other hand, in the basic first-order semantics one may expect there to be a model of $\mathsf {DCB}$ that neither satisfies $\mathsf {UBF}$ nor the equivalence between $\mathrm {CK}_A$ and $\mathrm {ICK}_A$ . Thus, the general predicate approach appears to offer a more nuanced setting, where these definitions of common knowledge can be logically distinguished from one another. Although further logico-philosophical research is required to uncover the precise relationship between these definitions of common knowledge, here follows a preliminary discussion on this matter.

         $\mathsf {UBF}$ formalizes the principle that whenever an agent knows the sentence “ $\phi (t)$ ” for all terms t, then the agent knows the sentence “ $\forall x \phi (x)$ ”. This makes sense in the arithmetic setting, where each standard natural number is referenced by a term. One may however envisage a scenario where the agent does not know that the collection of terms t, for which they know “ $\phi (t)$ ”, is the collection of all terms. One may also envisage a scenario where the agent does not know that every object is referenced by a term. ⁷ In either case, $\mathsf {UBF}$ needs to be rejected. If so, the equivalence between the fixed point definition and the iterated knowledge definition is in danger. However, as pointed out by an anonymous reviewer, it is not clear that there is an epistemically plausible situation where these definitions of common knowledge diverge extensionally. In particular, the instantiation of $\mathsf {UBF}$ used in the proof of Theorem 5(b) appears to be relatively uncontentious. This suggests that there is an epistemically well-motivated restriction of $\mathsf {UBF}$ , which does not have the contentious consequences that full $\mathsf {UBF}$ has, and which suffices to prove the equivalence of $\mathrm {CK}_A$ and $\mathrm {ICK}_A$ . Formulating and justifying such a restricted $\mathsf {UBF}$ is therefore an epistemically well-motivated avenue for further research. Note that a predicate approach is necessary for formalizing and reasoning about these matters.

      4. iv. An anonyomous reviewer pointed out a hybrid operator and predicate approach that goes back to an idea by Kripke in [15], namely to formalize truth by a predicate, $\mathrm {T}(x)$ , and knowledge by $\Box \mathrm {T}(x)$ , where $\Box $ is a model operator. This allows for addressing the paradoxes exclusively for truth, and formalizing knowledge in a manner that is not prone to inconsistency. In [20, §5], Stern shows that his modal system $\mathsf {MFS}$ can be “Kripke reduced” (in a certain precise sense) to a system that can be described as the Friedman–Sheard system of truth over quantified $\mathsf {S5}$ , in which necessity is formalized by $\Box \mathrm {T}(x)$ . As remarked by Stern in [20, pp. 274–275], there is conceptual merit to this reduction, as it establishes a correspondence with the hybrid approach that explains the consistency of the predicate approach, appealing to the confidence in the consistency of the operator approach. Thus, this benefit of the hybrid approach is also obtained in the predicate approach by means of the Kripke reduction. Since $\mathsf {KT} + \mathsf {UBF} + \mathsf {IA}$ is a close relative of $\mathsf {MFS}$ , one may expect that an analogous “Kripke reduction” is possible for $\mathsf {KT} + \mathsf {UBF} + \mathsf {IA}$ . An obstacle would be that $\mathsf {KT}$ is formulated for multi-agent knowledge, which cannot readily be formalized as a modal operator applied to a truth predicate. This could conceivably be remedied by switching to a plethora of operators, one for each agent. It is however not clear that common knowledge can be defined and reasoned with in such a system (without additional logical machinery), in analogy with the results in §3. In particular, my definition of common knowledge quantifies over the agents, which would not be possible. Moreover, it is hard to see how a knowledge predicate with an argument place for a justification could be reduced in such a manner. Finally, there are benefits to uniformly treating both knowledge and truth as predicates: only a first-order language is required, the simple first-order semantics applies, and methodological synergies are obtained as the two predicates can be studied with similar techniques.

   3. (c) Let us compare the two definitions of common knowledge, $\mathrm {CK}_A$ and $\mathrm {ICK}_A$ . $\mathrm {ICK}_A$ is a straight-forward and intuitive recursive definition, but it has the disadvantage of involving a rather complex quantification over an infinite collection of sentences. $\mathrm {CK}_A$ is arguably more succinct. Moreover, $\mathrm {CK}_A$ has the technical advantage of being workable by the proof-techniques of §3, based on Löb’s theorem. It also has an epistemic advantage highlighted in [4, chap. 11.5.1]: “[The fixed point] characterization of common knowledge […] is more directly related to the way common knowledge comes about and the way it is used.” This is explained in the context of a situation where a father makes an announcement to his children: “The reason why the statement is common knowledge can be intuitively described as follows: After the father speaks, the children are in a situation that can be characterized by the fact that they have all heard the father’s statement, and all know that they are in the situation.”

   4. (d) How do the results on common belief within $\mathsf {DCB}$ carry over to common knowledge within its super-system $\mathsf {KT}$ ? Most of the results of §3 are of the form “if $\mathsf {DCB}$ proves X, then $\mathsf {DCB}$ proves Y”. It is not possible to reformulate $\mathsf {KT}$ by substituting for $\mathsf {R}_{\mathsf {DCB}}$ , because by $\mathsf {V}$ and the axioms of truth, it would follow that $\neg {\Pr }_{\mathsf {KT} }(\bot )$ , contradicting Gödel’s second incompleteness theorem. Therefore, the proofs in §3 do not generalize to obtain “if $\mathsf {KT}$ proves X, then $\mathsf {KT}$ proves Y”. On the other hand, we obviously obtain “if $\mathsf {DCB}$ proves X, then $\mathsf {KT}$ proves Y”.Thus, Corollary 4 entails that whenever $\mathsf {DCB}$ proves that two formulas satisfy the fixed point condition ( $\mathsf {CBE}$ ), then $\mathsf {KT}$ proves them to be equivalent. However, by axioms $\mathsf {V}$ and $\mathsf {UCT}^{\mathrm {Atom}}$ , it can easily be checked that $\mathsf {KT}$ proves $\bot $ to satisfy ( $\mathsf {CBE}$ ), so formulas provably satisfying ( $\mathsf {CBE}$ ) in $\mathsf {KT}$ are not necessarily provably equivalent in $\mathsf {KT}$ . This suggests that $\mathsf {DCB}$ is the appropriate theory for defining the common knowledge fixed point, which can then be reasoned about in $\mathsf {KT}$ . In the case of Theorem 9 (c), its proof also only partially generalizes to obtain that for each $\phi \in \mathcal {L}^0$ and $A \in \mathcal {L}^1$ , $\mathsf {DCB} \vdash \phi \phantom {~~} \Longrightarrow \phantom {~~} \mathsf {KT} \vdash \mathrm {CK}_A(\ulcorner \phi \urcorner )$ . This raises the question of whether this result generalizes completely to $\mathsf {KT}$ or to an appropriate extension such as $\mathsf {KT} + \mathsf {UBF}$ . Taking a step back to assess the situation, it appears that the veracity axiom (which expresses the essential difference between belief and knowledge) leads to slightly different logical properties of the systems. A suggestion for further research is to investigate the correspondence between the philosophical and logical aspects of the veracity axiom, to explain this difference.

6. 6. Revision semantics: As shown in §4, $\mathsf {KT} + \mathsf {UBF} + \mathsf {IA}$ has a natural revision semantics, which generalizes both the traditional Hintikka-style possible worlds semantics for knowledge, ⁸ and the revision semantics for truth. Therefore, this predicate approach to epistemic logic is compatible with most of the development in the modal operator approach. A key insight of the paper, underpinning its development of this semantics, is that this semantics validates the self-referential axiom $\mathsf {R}_{\mathsf {DCB}}$ , which is instrumental to the results on common knowledge in §3.

7. 7. Discussion on $\mathsf {IA}$ : Consider the scenario of an agent who does not know that a particular name in fact refers to a true sentence, such as “ $0 = 0$ ”. This can be formalized by adding the following axioms to $\mathsf {KT}$ (but restricting $\mathsf {NEC}^{\mathrm {K}}$ to proofs in $\mathsf {KT}$ ), where s and a are constants: $s = \ulcorner \underline {0}=\underline {0} \urcorner $ , $\mathrm {Ag}(a)$ , $\neg \mathrm {K}(a, \ulcorner s = \ulcorner \underline {0}=\underline {0} \urcorner \urcorner )$ and $\neg \mathrm {K}(a, \ulcorner \mathrm {T}(s) \urcorner )$ . Working in this system, note that $\mathrm {K}(a, s)$ , by $\mathsf {NEC}^{\mathrm {K}}$ (and substitution of identicals), and that $\mathrm {T}\big (\ulcorner \mathrm {K}(a, s) \urcorner \big )$ , by $\mathsf {NEC}^{\mathrm {T}}$ . Moreover, we obtain that $\neg \mathrm {K}\big (a, \ulcorner \mathrm {K}(a, s) \urcorner \big )$ , by $\mathsf {V}$ , $\mathsf {NEC}^{\mathrm {K}}$ , $\mathsf {UK}^{\mathrm {K}}$ and $\neg \mathrm {K}(a, \ulcorner \mathrm {T}(s) \urcorner )$ . This example provides a counterexample both to $\mathsf {IA}$ and to the principle that whatever is known is known to be known. See also a similar example discussed in [22, §7.2], where the name “Goldbach’s conjecture” plays an analogous role to the constant s above. Still, $\mathsf {IA}$ is a well-motivated axiom under the simplifying assumption that all agents know each theorem of the system concerning syntax (in the counterexample, the agent a lacks knowledge about what sentence s refers to), otherwise it needs to be restricted in some way, cf. [22, §§7.3.2–7.3.3]. In [22], Stern provides a comprehensive discussion of this issue, along with a general approach to modify a range of possible worlds based semantics (such as that of §4) to accommodate this scenario. I have formulated $\mathsf {In}^+$ and $\mathsf {In}^-$ in such a way that they are compatible with this scenario. ⁹

8. 8. Inheritance from $\mathsf {FS}$ : Naturally, $\mathsf {KT}$ inherits many desirable properties from its subsystem $\mathsf {FS}$ . ¹⁰ (More generally, the predicate approach to modalities based on the system $\mathsf {FS}$ and the revision semantics, goes back to Stern’s [20]. ¹¹ ) In particular, its compositional axioms are philosophically well-motivated. Moreover, [10, corollary 14.24] shows that $\mathsf {FS}$ proves a large class of instances of Tarski’s schema $\mathrm {T}(\ulcorner \phi \urcorner ) \leftrightarrow \phi $ . ¹² Combining these two facts, $\mathsf {FS}$ gives a philosophical justification for these instances of that schema. As a consequence, $\mathsf {KT}$ both proves and philosophically justifies many instances of the schemata $\mathsf {UT}^{\mathrm {K}}$ and $\mathrm {K}[\mathsf {UT}^{\mathrm {K}}]$ in the knower paradoxes. Moreover, $\mathsf {KT} + \mathsf {In}^+$ proves and justifies many instances of the introspection schema $\mathrm {K}(\ulcorner \phi \urcorner ) \rightarrow \mathrm {K}(\ulcorner \mathrm {K}(\ulcorner \phi \urcorner ) \urcorner )$ . It is also worth noting that $\mathsf {FS}$ formalizes a conception of truth which follows classical logic, and is unambiguous in the sense that any $\phi \in \mathcal {L}^0$ is proved “externally true” (i.e., $\mathsf {FS} \vdash \phi $ ) iff it is proved “internally true” (i.e., $\mathsf {FS} \vdash \mathrm {T}(\ulcorner \phi \urcorner )$ ). These properties set $\mathsf {FS}$ apart from $\mathsf {KF}$ , another prominent system of untyped truth. ¹³

Another avenue for further research is to look for more applications of the techniques utilized in §3. In particular, are there other useful definitions to be made as Gödel fixed points, and are there positive applications of Löb’s theorem to be obtained concerning them?