# 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 present it here:

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

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

Thanks very much.

-

## closed as too localized by Andrés E. Caicedo, Steven Landsburg, Todd Trimble♦, George Lowther, GoldsternOct 18 '12 at 0:06

This question is unlikely to help any future visitors; it is only relevant to a small geographic area, a specific moment in time, or an extraordinarily narrow situation that is not generally applicable to the worldwide audience of the internet. For help making this question more broadly applicable, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

Voting to close because the phrasing strongly suggests that this is homework. – Steven Landsburg Oct 17 '12 at 19:08
Dear @Incnis Mrsi, please do not edit more than three old questions each day, as they take up space on the front page. Check the meta thread meta.mathoverflow.net/questions/599/… for more information. Thank you. – Ricardo Andrade Dec 18 '14 at 23:26

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 '12 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 '12 at 1:30
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 '12 at 11:50