A question on intuitionistic propositional logic - MathOverflow [closed]most recent 30 from http://mathoverflow.net2013-05-23T08:16:48Zhttp://mathoverflow.net/feeds/question/109930http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/109930/a-question-on-intuitionistic-propositional-logicA question on intuitionistic propositional logicSet2012-10-17T17:38:56Z2012-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#109938Answer by Emil Jeřábek for A question on intuitionistic propositional logicEmil Jeřábek2012-10-17T19:00:30Z2012-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>