Use induction on the complexity of $C$ to prove that if $K\vdash A\leftrightarrow B$ then $K\vdash C[A/q]\leftrightarrow C[B/q]$
This is question 3.3 from OLP's Boxes and Diamonds.
I have found proofs for the base cases, where $C\equiv\top$, $C\equiv\bot$, and $C\equiv p_n$. In each case, $C\equiv C[A/q]\equiv C[B/q]$ since $q$ cannot occur in $\top,\bot,$ or $p_n$. So $C[A/q]\leftrightarrow C[B/q]$ is a tautology in each case and so $K\vdash C[A/q]\leftrightarrow C[B/q]$.
What I struggling with is the inductive step. As hypothesis, I assume that, given $K\vdash A\leftrightarrow B$, $K\vdash C[A/q]\leftrightarrow C[B/q]$ and $K\vdash D[A/q]\leftrightarrow D[B/q]$ for arbitrary formula $C,D$.
What I then need to show is that, on this supposition:
- $K\vdash \lnot C[A/q]\leftrightarrow \lnot C[B/q]$
- $K\vdash ( C[A/q]\land D[A/q])\leftrightarrow (C[B/q]\land D[B/q])$
- $K\vdash ( C[A/q]\lor D[A/q])\leftrightarrow (C[B/q]\lor D[B/q])$
- $K\vdash ( C[A/q]\rightarrow D[A/q])\leftrightarrow (C[B/q]\rightarrow D[B/q])$
- $K\vdash ( C[A/q]\leftrightarrow D[A/q])\leftrightarrow (C[B/q]\leftrightarrow D[B/q])$
- $K\vdash \Box C[A/q]\leftrightarrow \Box C[B/q]$
- $K\vdash \Diamond C[A/q]\leftrightarrow \Diamond C[B/q]$
Working on the first one, the negation case, I supposed $K\nvdash \lnot C[A/q]\leftrightarrow \lnot C[B/q]$ and then inferred that if so, either: 1) $K\vdash \lnot C[A/q]$ and $K\nvdash \lnot C[B/q]$ or 2) $K\nvdash \lnot C[A/q]$ and $K\vdash \lnot C[B/q]$. Regarding 1, if $K\vdash \lnot C[A/q]$, then $K\nvdash C[A/q]$. And so, by the inductive hypothesis, $K\nvdash C[B/q]$. But then $K\vdash \lnot C[B/q]$. Contradiction. And case 2 follows an analogous path.
My question is whether this reasoning is legitimate. In particular, can I suppose that if $K\nvdash\alpha\leftrightarrow\beta$ then either $K\vdash\alpha$ and $K\nvdash\beta$ or $K\nvdash\alpha$ and $K\vdash\beta$?
If not, any hints for alternative strategies? Thanks so much. I really appreciate the help!