I've been reading The Logic of Provability by George Boolos, and something he said stumped me for a bit.
Let us use H (for Henkin) to refer to the system that results when (YS) is added to K, i.e., H is the normal system whose new axioms are all sentences $\Box(A \leftrightarrow \Box A)\rightarrow\Box A$. H is clearly a proper extension of K, since $\Box(p \leftrightarrow \Box p)\rightarrow\Box p$ is not a theorem of K. For let $M = \langle N,<,V\rangle$, where for all $n$ in $N$, not: $nVp$. Then $p$ is false, $\Box p$ is false, $p\leftrightarrow\Box p$ is true, $\Box(p\leftrightarrow\Box p)$ is true, and therefore $\Box(p\leftrightarrow\Box p)\rightarrow\Box p$ is false, at all $n$ in $M$.
Why can't that argument be used in a model of GL? That is, what is it about GL's models (transitive, irreflexive, converse wellfounded ones) that makes the above argument fail?
Ok I got it. If $p$ is false at all worlds, then at a "bottommost" world $n$, $n\models\neg p$ and $n\models\square p$, and $n\models\neg(p\leftrightarrow\square p)$ and therefore (from transitivity and converse wellfoundedness) $0 \not\models\square(p\leftrightarrow\square p)$ (where $0$ is the "first" world) whence $0\models \square(p\leftrightarrow\square p) \rightarrow\square p$.
And we can reason inductively from there to prove that no matter what, it will always be the case that $0\models \square(p\leftrightarrow\square p) \rightarrow\square p$.
Okay.