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!