[proofplan] We prove persistence by structural induction on the formula $A$. Atomic formulas use the atomic persistence hypothesis, and the constants and binary connectives follow directly from their forcing clauses. The implication case uses transitivity of the preorder: every extension of $u$ is also an extension of $w$. [/proofplan] [step:Set up structural induction on the formula] Fix worlds $w,u \in K$ with $w \le u$. We prove, by structural induction on $A \in \mathrm{Form}$, that $w \Vdash A$ implies $u \Vdash A$. The induction predicate $P(A)$ is the statement that for every pair $w,u \in K$, if $w \le u$ and $w \Vdash A$, then $u \Vdash A$. Since $\mathrm{Form}$ is generated from propositional variables, $\bot$, $\top$, $\land$, $\lor$, and $\to$, it is enough to prove $P(A)$ for each generator and show that $P$ is preserved by the three binary constructors. [/step] [step:Use atomic persistence and the forcing clauses for constants] Let $p \in \mathrm{Prop}$ be a propositional variable. If $w \le u$ and $w \Vdash p$, then $w \Vdash_{\mathrm{At}} p$ by the atomic forcing clause. Atomic persistence gives $u \Vdash_{\mathrm{At}} p$, hence $u \Vdash p$. Therefore $P(p)$ holds. For $\bot$, the implication from $w \Vdash \bot$ to $u \Vdash \bot$ has an impossible antecedent, since no world forces $\bot$. Therefore $P(\bot)$ holds. For $\top$, every world forces $\top$ by definition, so $u \Vdash \top$ for every $u \in K$. Therefore $P(\top)$ holds. [guided] The atomic case is where the hypothesis on $\Vdash_{\mathrm{At}}$ is used. Take $p \in \mathrm{Prop}$ and worlds $w,u \in K$ with $w \le u$. If $w \Vdash p$, then the recursive definition of forcing says exactly that $w \Vdash_{\mathrm{At}} p$. Atomic persistence then gives $u \Vdash_{\mathrm{At}} p$, and the atomic forcing clause converts this back to $u \Vdash p$. The constants use their defining clauses. There is no world $w \in K$ with $w \Vdash \bot$, so the implication defining $P(\bot)$ has no forcing instance to check. For $\top$, the definition says every world forces $\top$, so in particular $u \Vdash \top$. Thus both constants are persistent. [/guided] [/step] [step:Pass persistence through conjunction and disjunction] Assume $P(B)$ and $P(C)$. If $w \le u$ and $w \Vdash B \land C$, then $w \Vdash B$ and $w \Vdash C$. Applying $P(B)$ to $w \le u$ gives $u \Vdash B$, and applying $P(C)$ to $w \le u$ gives $u \Vdash C$. Hence $u \Vdash B \land C$. If $w \le u$ and $w \Vdash B \lor C$, then either $w \Vdash B$ or $w \Vdash C$. In the first case, $P(B)$ gives $u \Vdash B$, hence $u \Vdash B \lor C$. In the second case, $P(C)$ gives $u \Vdash C$, hence $u \Vdash B \lor C$. Thus $P(B \lor C)$ holds. [/step] [step:Use transitivity to handle implication] Assume $P(B)$ and $P(C)$. Suppose $w \le u$ and $w \Vdash B \to C$. To show $u \Vdash B \to C$, let $v \in K$ satisfy $u \le v$ and $v \Vdash B$. Since $(K,\le)$ is a preorder, $\le$ is transitive. From $w \le u$ and $u \le v$, we get $w \le v$. The forcing clause for $w \Vdash B \to C$ now applies to this world $v$: because $w \le v$ and $v \Vdash B$, it follows that $v \Vdash C$. Since every $v \in K$ with $u \le v$ and $v \Vdash B$ also satisfies $v \Vdash C$, the implication forcing clause gives $u \Vdash B \to C$. Therefore $P(B \to C)$ holds. [/step] [step:Conclude persistence for all formulas] The structural induction has established $P(A)$ for every $A \in \mathrm{Form}$. Unwinding the definition of $P(A)$, for all worlds $w,u \in K$, if $w \le u$ and $w \Vdash A$, then $u \Vdash A$. This is the claimed persistence of forcing. [/step]