# A question on intuitionistc propositional logic

Prove that:

Two finite rooted frames are isomorphic iff they validate the same formulas.

(This is an exercise in the book "Modal Logic" by A.Chagrov and M.Zakharyaschev)

• What kind of frames, what kind of formulas are we talking about? Do we have one modality (one relation on frames)? Are reflexivity and/or transitivity (S4) assumed? – Berci Oct 8 '12 at 9:58
• @Berci . The language of intuitionistc propositional logic is same as the language of classical propositional logic. And the frames are all partial ordered frames. – Sencodian Oct 8 '12 at 10:21
• Ah, sorry, this booktitle "Modal Logic" misled me... So, then.. what is a 'rooted frame' and the semantics? – Berci Oct 8 '12 at 10:33
• @Berci . See the item "Semantics of intuitionistic logic" in the following website: en.wikipedia.org/wiki/Kripke_semantics – Sencodian Oct 8 '12 at 10:56
• To understand the question, it is important to know that the definition of "rooted frame" is that every node is accessible from the "root" with one or more steps. So "rooted" does not just mean "pointed" as might be expected; "rooted" affects both the order structure of the frame and the choice of a root node. – Carl Mummert Jul 22 '13 at 11:49

The key-phrase here is `Jankov-Fine formulas'. See Theorem 95 and Exercise 98 here: http://www.illc.uva.nl/Research/Reports/PP-2006-25.text.pdf. So, by Theorem 95, if $F$ and $G$ are finite rooted frames which validate the same formulas, each of them is a $p$-morphic image of a generated subframe of the the other. By Exercise 98, this implies that they are isomorphic.
• !tci: I answered one of my questions about this, but I have one more. Suppose I have a finite rooted frame, which happens to be a tree, with root $r$. For each child $c$ of $r$, I duplicate the entire subtree of the frame starting with $c$ and make that a new subtree below $r$. Now the root of the new frame will force the same formulas as the root of the old frame, but the new frame is not isomorphic. So there must also be some extensionality condition on the frame to get the result to go through? – Carl Mummert Jul 22 '13 at 11:37