Inductive Proof of $(M^c,s_V)\vDash\varphi$ iff $\varphi\in V$ (Modal Case)

Question

This post is regarding the proof of $(M^c,s_V)\vDash\varphi$ iff $\varphi\in V$ in Reasoning about Knowledge, by Fagin, Halpern, Moses, & Vardi. This is used in showing that K$_n$ is a sound and complete axiomatization with respect to $\mathcal M_n$ for formulas in the language $\mathcal L_n$.

I need help understanding the modal case of the inductive proof of $(M^c,s_V)\vDash\varphi$ iff $\varphi\in V$ ($\color{red}{\text{highlighted in red}}$ below), but I shall provide the entire proof of Theorem $3.1.3$ for context.

---

Theorem: K$_n$ is a sound and complete axiomatization with respect to $\mathcal M_n$ for formulas in the language $\mathcal L_n$.
Proof:
It is easy to prove by induction on the length of proof of $\varphi$ that if $\varphi$ is provable in K$_n$, then $\varphi$ is valid with respect to $\mathcal{M}_n$. It follows that K$_n$ is sound with respect to $\mathcal{M}_n$.

To prove completeness, we must show that every formula in $\mathcal{L}_n$ that is valid with respect to $\mathcal{M}_n$ is provable in K$_n$. It suffices to prove that $$\begin{align} \text{Every K}_n\text{-consistent formula in }\mathcal{L}_n\text{ is satisfiable with respect to}\mathcal{M}_n. \quad(\bigstar) \end{align}$$ Suppose we can prove $(\bigstar)$, and $\varphi$ is a valid formula in $\mathcal{L}_n$. If $\varphi$ is not provable in K$_n$, then neither is $\lnot\lnot \varphi$. By definition, $\lnot\varphi$ is K$_n$-consistent. It follows from $(\bigstar)$ that $\lnot\varphi$ is satisfiable with respect to $\mathcal{M}_n$, contradicting the validity of $\varphi$ with respect to $\mathcal{M}_n$.

We prove $(\bigstar)$ by constructing a special structure $M^c\in\mathcal{M}_n$, called the canonical structure for K$_n$. $M^c$ has a state $s_V$ corresponding to every maximal K$_n$ consistent set $V$. Then we show $$\begin{align} (M^c,s_V)\vDash \varphi \text{ if and only if }\varphi\in V. \quad(\bigstar\bigstar) \end{align}$$ Note that $(\bigstar\bigstar)$ is sufficient to prove $(\bigstar)$, for if $\varphi$ is K$_n$-consistent, then $\varphi$ is contained in some maximal K$_n$-consistent set $V$. From $(\bigstar\bigstar)$ it follows that $(M^c,s_V)\vDash\varphi$ and so $\varphi$ is satisfiable in $M^c$. Therefore, $\varphi$ is satisfiable with respect to $\mathcal{M}_n$, as desired.

Given a set $V$ of formulas, define $K/V_i = \{\varphi: K_i\varphi\in V\}$. Let $M^c = (S,\pi,R_1,\ldots, R_n)$ where $$\begin{align*} S &= \{s_V: V \text{ is a maximal K$_n$-consistent set} \}\\ \pi(s_V)(p) &= \begin{cases}T & \text{if }p\in V\\ F& \text{if }p\notin V\end{cases}\\ R_i = \{(s_V,s_W): V/K_i \subseteq W\}. \end{align*}$$ We now show that for every $s_V\in S$ we have $(M^c,s_V)\vDash\varphi$ if and only if $\varphi\in V$. We proceed by induction on the structure of formulas. Assuming that the claim holds for all subformulas of $\varphi$, we show that it also holds for $\varphi$.

If $\varphi$ is a primitive proposition $p$, the claim follows immediately from the definition of $\pi(s_V)$.

Suppose $\varphi = \psi_1 \land \psi_2$. $(M^c,s_V)\vDash \psi_1\land\psi_2$ iff $(M^c,s_V)\vDash\psi_1$ and $(M^c,s_V)\vDash\psi_2$. By the induction hypothesis, $(M^c,s_V)\vDash\psi_1$ iff $\psi_1\in V$ and $(M^c,s_V)\vDash\psi_2$ iff $\psi_2\in V$. Since $V$ is maximally K$_n$-consistent, $\psi_1\in V$ and $\psi_2\in V$ iff $\psi_1\land\psi_2\in V$. As a result, $(M^c,s_V)\vDash \psi_1\land\psi_2$ if and only if $\psi_1\land\psi_2\in V$.

Suppose $\varphi = \lnot\psi$. $(M^c,s_V)\vDash \lnot\psi$ iff $(M^c,s_V)\not\vDash\psi$. By the induction hypothesis, $(M^c,s_V)\not\vDash\psi$ iff $\psi\notin V$. Since $V$ is maximally K$_n$-consistent, $\psi\notin V$ iff $\lnot\psi\in V$. So, $(M^c,s_V)\vDash \lnot\psi$ if and only if $\lnot\psi\in V$.

Suppose $\varphi = K_i\psi$ and $\varphi\in V$. Then, $\psi\in V/K_i$ and by the definition of $R_i$, if $(s_V,s_W)\in R_i$ then $\psi\in W$. Thus, by using the induction hypothesis, $(M^c,s_W)\vDash\psi$ for all $W$ such that $(s_V,s_W)\in R_i$. By definition of $\vDash$, it follows that $(M^c,s_V)\vDash K_i\psi$.

$\color{red}{\text{The forward direction of the modal case begins here.}}$
$\color{red}{\text{This is the part I need help with. Everything before this is only for context.}}$

Suppose $\varphi = K_i\psi$ and $(M^c,s_V)\vDash K_i\psi$. It follows that the set $(V/K_i)\cup\{\lnot\psi\}$ is not K$_n$-consistent. For suppose otherwise. Then it would have a maximal K$_n$-consistent extension $W$ and, by construction, we would have $(s_V,s_W)\in R_i$. By the induction hypothesis, we have $(M^c,s_W)\vDash\lnot\psi$ and so $(M^c,s_V)\vDash \lnot K_i\psi$, contradicting our original assumption. Since $(V/K_i)\cup\{\lnot\psi\}$ is not K$_n$-consistent, there must be some finite subset say $\{\varphi_1,\ldots,\varphi_k,\lnot\psi\}$ which is not K$_n$-consistent. Thus, by propositional reasoning, we have $$\text{K}_n\vdash \varphi_1 \to (\varphi_2 \to (\ldots \to (\varphi_k\to\psi)\ldots)).$$

1. How do we arrive at $\text{K}_n\vdash \varphi_1 \to (\varphi_2 \to (\ldots \to (\varphi_k\to\psi)\ldots))$? Could someone kindly provide a detailed argument?

By the Knowledge Generalization Axiom, we have $$\text{K}_n\vdash K_i(\varphi_1 \to (\varphi_2 \to (\ldots \to (\varphi_k\to\psi)\ldots))).$$ By induction on $k$, together with axiom (A2) and propositional reasoning, we can show $$\text{K}_n\vdash K_i(\varphi_1\to (\varphi_2 \to (\ldots \to (\varphi_k\to \psi)\ldots )) \implies (K_i\varphi_1\to (K_i\varphi_2 \to (\ldots \to (K_i\varphi_k\to K_i\psi)\ldots))).$$

2. What exactly is the induction argument involved here? Could someone please help fill in the details?

Now from Modus Ponens we get $$\text{K}_n\vdash K_i\varphi_1\to (K_i\varphi_2 \to (\ldots \to (K_i\varphi_k\to K_i\psi)\ldots))$$ $K_i\varphi_1\to (K_i\varphi_2 \to (\ldots \to (K_i\varphi_k\to K_i\psi)\ldots)) \in V$. Since $\varphi_1,\ldots,\varphi_k\in V/K_i$, we must have $K_i\varphi_1, \ldots, K_i\varphi_k \in V$. It follows that $K_i\psi\in V$ as desired.

Thanks a lot! I know this is a really long post, but I'd really appreciate any help with my two questions!

Answer 1

1. ad Q1

Suppose $\{ \varphi_1, \ldots, \varphi_k, \neg \psi \}$ is a $K_n$-inconsistent subset of $V/K_i \cup \{ \neg \psi \}$. Then

$\vdash_{K_n} \neg(\varphi_1 \wedge \ldots \wedge \varphi_k \wedge \neg \psi)$.

By propositional reasoning we have that

$\vdash_{K_n} \neg \varphi_1 \lor \ldots \lor \neg \varphi_k \lor \psi$.

Since $\vdash_{K_n} (\neg \varphi_k \lor \psi) \leftrightarrow (\varphi_k \rightarrow \psi)$, we can conclude that

$\vdash_{K_n} \neg \varphi_1 \lor \ldots \lor \neg \varphi_{k-1} \lor (\varphi_k \rightarrow \psi)$.

Again, as $\vdash_{K_n} (\neg \varphi_{k-1} \lor (\varphi_k \rightarrow \psi)) \leftrightarrow (\varphi_{k-1} \rightarrow (\varphi_k \rightarrow \psi))$ it follows that

$\vdash_{K_n} \neg \varphi_1 \lor \ldots \lor \neg \varphi_{k-2} \lor (\varphi_{k-1} \rightarrow (\varphi_k \rightarrow \psi))$.

Iterating this procedure $k-2$ times we arrive at

$\vdash_{K_n} \varphi_1 \rightarrow (\varphi_2 \rightarrow (\ldots \rightarrow(\varphi_k \rightarrow \psi) \ldots))$.

2. ad Q2

The induction base is trivial: For $k=1$ the desired result, namely

$\vdash_{K_n} K_i(\varphi_1 \rightarrow \psi) \rightarrow (K_i \varphi_1 \rightarrow K_i \psi)$,

is an instance of the K-axiom. For the induction step, assume the claim holds for all $n < k$. We show it also holds for $k$ by constructing a $K_n$-proof (some notes on proof presentation: every numbered line is thought to the claim that the formula in that line is $K_n$-provable; justifications for provability claims are given at the end of each line; the label PC means that the provability claim is justified by propositional reasoning):

1. $K_i(\varphi_1 \rightarrow ( \varphi_2 \rightarrow( \ldots \rightarrow ( \varphi_k \rightarrow \psi) \ldots))) \rightarrow (K_i\varphi_1 \rightarrow K_i( \varphi_2 \rightarrow( \ldots \rightarrow ( \varphi_k \rightarrow \psi) \ldots)))$, K-axiom

2. $K_i(\varphi_2 \rightarrow( \ldots \rightarrow ( \varphi_k \rightarrow \psi) \ldots)) \rightarrow (K_i\varphi_2 \rightarrow( \ldots \rightarrow (K_i \varphi_k \rightarrow K_i \psi)))$, induction hypothesis

3. $K_i \varphi_1 \rightarrow (K_i( \varphi_2 \rightarrow (\ldots \rightarrow (\varphi_k \rightarrow \psi ) \ldots )) \rightarrow [K_i \varphi_1 \rightarrow (K_i \varphi_2 \rightarrow (\ldots \rightarrow (K_i\varphi_k \rightarrow K_i \psi)))]$, PC 2

4. $K_i(\varphi_1 \rightarrow ( \varphi_2 \rightarrow( \ldots \rightarrow ( \varphi_k \rightarrow \psi) \ldots)))\rightarrow [K_i \varphi_1 \rightarrow (K_i \varphi_2 \rightarrow (\ldots \rightarrow (K_i\varphi_k \rightarrow K_i \psi)))]$, PC 1,3

Answer 2

Let me provide a lazy answer in a sense that, instead of trying to work through the proof from the textbook, I will provide the one I like and use.

So, the truth lemma goes as follows:

Truth Lemma For all mcs' $\Gamma$ and all $\varphi \in \mathcal{K}$ (the language of logic $\mathbf{K}$) it holds that $\varphi \in \Gamma$ iff $\mathfrak{M}^C_{\Gamma} \models \varphi$ ($\varphi$ holds in state $\Gamma$ of the canonical model).

Proof. Base case follows from the definition of the canonical model.

Induction hypothesis. For all proper subformulas $\psi$ of $\varphi$ we have that $\psi \in \Gamma$ iff $\mathfrak{M}^c_{\Gamma} \models \psi$. (I assume that the subformula relation is defined as a well-founded strict partial order)

Case $\psi:= \square_a \chi$. From left to right: Assume that $\square_a \chi \in \Gamma$. By the definition of the canonical model this means that $\chi \in \Delta$ for all $\Delta$ such that $\Gamma \setminus \square_a \subseteq \Delta$. By the induction hypothesis and the definition of the canonical model, the latter is equivalent to $\mathfrak{M}^c_\Delta \models \chi$ for all $\Delta$ such that $\Gamma \sim_a \Delta$. Finally, the latter is equivalent to $\mathfrak{M}^c_{\Gamma} \models \square_a \chi$ by the semantics.

From right to left: Assume that $\mathfrak{M}^c_{\Gamma} \models \square_a \chi$. By the semantics this is equivalent to the fact that for all $\Delta$ such that $\Gamma \sim_a \Delta$, $\mathfrak{M}^c_{\Delta} \models \chi$. By the definition of the canonical model and the induction hypothesis, the latter is equivalent to the fact that for all $\Delta$ such that $\Gamma \setminus \square_a \subseteq \Delta$, $\chi \in \Delta$. Now we need to show that $\square_a \chi \in \Gamma$. Suppose towards a contradiction that $\square_a \chi \not \in \Gamma$, and hence $\chi \not \in \Gamma \setminus \square_a$.

Small fact about $\Gamma \setminus \square_a$: set $\Gamma \setminus \square_a$ contains all theorems of $\mathbf{K}$ and is closed under R1. This can be shown using the fact that if some $\tau$ is a theorem, $\square_a \tau$ is a theorem as well, and using the distributivity of $\square_a$.

Another useful sublemma: $\Gamma \setminus \square_a \cup \{\tau\}$ is consistent iff $\lnot \tau \not \in \Gamma \setminus \square_a$. This can be shown using the fact that $\Gamma \setminus \square_a \subseteq \Gamma \setminus \square_a \cup \{\tau\}$.

Once we have this, the proof follows easily. Recall that we have $\chi \not \in \Gamma \setminus \square_a$. By another useful lemma, this is equivalent to $\Gamma \setminus \square_a \cup \{\lnot \chi\}$ being consistent. Then, according to Lindenbaum Lemma, this consistent set can be extended to a mcs $\Delta^\prime$ such that $\Gamma \setminus \square_a \subseteq \Delta^\prime$ and $\lnot \chi \in \Delta^\prime$. A contradiction.