Theorem 28

We prove the first correspondence. That is, we shall show that $\alpha$ is K$_N$-provable if and only if $tr(\alpha)$ is K$^A_N$-provable. The other results are obtained in the same way.

First, we show that the translation of every K$_N$-theorem is a K$^A_N$-theorem. Let $\alpha$ be a theorem of K$_N$. We show inductively over the length of the proof of $\alpha$ in K$_N$ that $tr(\alpha)$ is a theorem of K$^A_N$.

Assume that $\alpha$ is one of K$_N$-axioms, i.e., it is either a propositional tautology or an instance of the schema K. In the former case $tr(\alpha)$ is also a propositional tautology, and in the latter case $tr(\alpha)$ is an instance of (K$^A$), so in any case $tr(\alpha)$ is a K$^A_N$-theorem.

Now suppose that $\alpha$ has been derived by applying modus ponens to $\beta$ and $\beta \to \alpha$. By induction hypothesis, both $tr(\beta)$ and $tr(\beta \to \alpha)$ are K$^A_N$-theorems. By definition, $tr(\beta \to \alpha)$ is $tr(\beta) \to tr(\alpha)$, so in K$^A_N$ we can apply modus ponens to infer $tr(\alpha)$.

Finally, suppose that $\alpha$ has been derived from $\beta$ using the knowledge necessitation rule (NEC), i.e., $\alpha$ is $K_i\beta$ and $\beta$ is a K$_N$-theorem. Then $tr(\beta)$ is a theorem of K$^A_N$, by induction hypothesis. According to the definition of $tr$, $tr(\alpha)$ is $K_i^{\exists} tr(\beta)$, which can be derived from the theorem $tr(\beta)$ by applying the rule (NEC$^A$). Hence, $tr(\alpha)$ is a K$^A_N$-theorem.

To prove the converse, we define the inverse function $tr^{-1}: \mathcal{L}_{N}^{AK} \mapsto \mathcal{L}_{N}^{K}$ of $tr$ as follows:

• $tr^{-1}(\phi) = \phi$ for all $\phi \in Atom$

• $tr^{-1}(\lnot \alpha) = \lnot tr^{-1}(\alpha)$

• $tr^{-1}(\alpha \to \beta) = tr^{-1}(\alpha) \to tr^{-1}(\beta)$

• $tr^{-1}(K_i^n\alpha) = K_i(tr^{-1}(\alpha))$, for all $n\in \omega$

• $tr^{-1}(K_i^{\exists}\alpha) = K_i(tr^{-1}(\alpha))$

It is easy to see that $tr^{-1}(tr(\alpha)) = \alpha$ for all $\alpha \in \mathcal{L}_{N}^{K}$. However, the converse does not hold: generally $tr(tr^{-1}(\alpha))$ and $\alpha$ are different formulae. For instance, $tr(tr^{-1}(K_i^n\phi)) = tr(K_i(tr^{-1}(\phi))) = tr(K_i\phi) = K_i^{\exists}\phi \neq K_i^n\phi$.

Assume that $tr(\alpha)$ is provable in K$^A_N$. Then there is a K$^A_N$-proof leading to $tr(\alpha)$, i.e., there is a sequence $\beta_0,\ldots,\beta_n$ of K$^A_N$-formulae such that $\beta_n$ is $tr(\alpha)$ and each $\beta_k$ ($k=0,\ldots,n$) is either an axiom of K$^A_N$ or is derived from previous formulae in the sequence using one of the inference rules. We show that the sequence $tr^{-1}(\beta_0), \ldots, tr^{-1}(\beta_n)$ is a proof of $\alpha$ in K$_N$.

Suppose that $\beta_k$ is axiom of K$^A_N$. If $\beta_k$ is a propositional tautology then so is $tr^{-1}(\beta_k)$. If $\beta_k$ is an instance of (K$^A$) then $tr^{-1}(\beta_k)$ is an instance of (K). If $\beta_k$ is an instance of (P$^A$) or (Q$^A$) then $tr^{-1}(\beta_k)$ is a propositional tautology.

Suppose that $\beta_k$ is derived from $\beta_l$ and $\beta_l \to \beta_k$ by modus ponens. Then $tr^{-1}(\beta_l)$ and $tr^{-1}(\beta_l \to \beta_k)$ are K$_N$-theorems, so $tr^{-1}(\beta_k)$ can be inferred from $tr^{-1}(\beta_l)$ and $tr^{-1}(\beta_l) \to tr^{-1}(\beta_k)$ (which is by definition the same formula as $tr^{-1}(\beta_l \to \beta_k)$.)

Finally, let $\beta_k$ be derived from $\beta_l$ by applying (NEC$^A$). Then $\beta_k$ is $K_i^{\exists}\beta_l$, hence $tr^{-1}(\beta_k)$ is $K(tr^{-1}(\beta_l))$, which can be derived from $tr^{-1}(\beta_l)$ using (NEC).

Thus, in any case $tr^{-1}(\beta_k)$ is a theorem of K$_N$. As observed earlier, $tr^{-1}(\beta_n) = tr^{-1}(tr(\alpha)) = \alpha$. So $\alpha$ is a theorem of K$_N$. This completes the proof.