0
$\begingroup$

One week ago, I asked a question on math.stackexchange.com (https://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.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Voting to close because the phrasing strongly suggests that this is homework. $\endgroup$
    – Steven Landsburg
    Commented Oct 17, 2012 at 19:08
  • $\begingroup$ 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. $\endgroup$
    – Ricardo Andrade
    Commented Dec 18, 2014 at 23:26

1 Answer 1

Reset to default
0
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$
    – Set
    Commented Oct 18, 2012 at 1:24
  • $\begingroup$ 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. $\endgroup$
    – Set
    Commented Oct 18, 2012 at 1:30
  • $\begingroup$ 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). $\endgroup$
    – Emil Jeřábek
    Commented Oct 18, 2012 at 11:36
  • $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Oct 18, 2012 at 11:50

Not the answer you're looking for? Browse other questions tagged .