Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question

closed as too localized by Andres Caicedo, Steven Landsburg, Todd Trimble, George Lowther, Goldstern Oct 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.

1  
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 at 23:26

1 Answer 1

up vote 0 down vote accepted

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.

share|improve this answer
    
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
    
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 '12 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 '12 at 11:50

Not the answer you're looking for? Browse other questions tagged or ask your own question.