A question on intuitionistic propositional logic [closed]

One week ago, I asked a question on math.stackexchange.com (http://math.stackexchange.com/questions/209120/a-question-on-intuitionistc-propositional-logic) . But nobody answered my question. So I presented it here:

In the Kripke's semantics of intuitionistic propositional logic, the frames are all partial ordered frames. Prove that:

Two finite rooted frames are isomorphic iff they validate the same formulas in the langusge of intuitionistic propositional logic.

Thanks very much.

-
Voting to close because the phrasing strongly suggests that this is homework. – Steven Landsburg Oct 17 at 19:08

closed as too localized by Andres Caicedo, Steven Landsburg, Todd Trimble, George Lowther, GoldsternOct 18 at 0:06

Let $F,G$ be the two frames. Let $\beta$ be the frame formula of $F$ (using notation from the Chagrov and Zakharyaschev book you mention in the MSE question, $\beta=\beta^\sharp(F,\bot)$). Since $\beta$ is refutable in $F$, it is also refutable in $G$, hence there exists a generated subframe $H\subseteq G$ and a surjective p-morphism $f\colon H\to F$. A symmetric argument shows that $F$ is a p-morphic image of a generated subframe of $G$, hence $|F|\le|G|$. This in turn implies that $|H|=|G|=|F|$, and as the frames are finite, this can only happen if $H=G$ and $f$ is a bijection. Thus, $f$ is an isomorphism.
 Thank you very much. In Chagrov's excellent book, this exercise is in Chapter 2 but the notation "the frame formula of $F$" is in chapter 9. What is the author's intention? – Set Oct 18 at 1:24 I want to ask another question on modal logic: Show that the set of pretabular logics in NEx$tK4BD_n$ is finite for every $n<\omega$ and that all of them are finitely axiomatizable. – Set Oct 18 at 1:30 Well, the exercises in C&Z are sometimes quite tough. I’m not aware of any essentially different method of proving the isomorphism, and there are no techniques introduced in Chapter 2 that would be sufficient. Maybe they do intend for the reader to invent frame formulas themselves (the needed property is fairly basic, one does not need the full machinery of Ch. 9 for that). – Emil Jeřábek Oct 18 at 11:36 As for pretabular logics, there is no short answer. You apply the same method as in Thm. 12.13 or 12.16: a nontabular logic extending K4BD_n has finite frames of unbounded cluster size or unbounded width, and you try to sort of minimize the set of frames with this property. (This is not a terribly difficult exercise after reading section 12.3, but it’s rather tedious.) I’d guess the result should include logics of frames consisting of an infinite cluster sitting below a generated subframe of the universal frame $F_{K4}^{< n}(0)$, and something similar with infinite width. – Emil Jeřábek Oct 18 at 11:50