A question on intuitionistic propositional logic - MathOverflow [closed] most recent 30 from http://mathoverflow.net 2013-05-23T08:16:48Z http://mathoverflow.net/feeds/question/109930 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/109930/a-question-on-intuitionistic-propositional-logic A question on intuitionistic propositional logic Set 2012-10-17T17:38:56Z 2012-10-17T19:00:30Z <p>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:</p> <p>In the Kripke's semantics of intuitionistic propositional logic, the frames are all partial ordered frames. Prove that:</p> <p>Two finite rooted frames are isomorphic iff they validate the same formulas in the langusge of intuitionistic propositional logic.</p> <p>Thanks very much.</p> http://mathoverflow.net/questions/109930/a-question-on-intuitionistic-propositional-logic/109938#109938 Answer by Emil Jeřábek for A question on intuitionistic propositional logic Emil Jeřábek 2012-10-17T19:00:30Z 2012-10-17T19:00:30Z <p>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.</p>