Proove that all finite non-standard Kripke frames are standard

134 Views Asked by At

In Harel's book on PDL (Propositional Dynamic Logic) I've learnt that Kripke frames are pairs such as: K = (K; $m_k$)

Where $K$ is a set called states and $m_k$ is a meaning function assigning subset of $K$ to each atomic proposition and a binary relation on $K^2$ to each atomic program: $m_k$ ($p$) $\subset$ $K$, where $p$ is an atomic formula; $m_k$ ($\alpha$) $\subset$ $K^2$, where $\alpha$ is an atomic program.

By definition, we have:

$$m_k(\phi->\psi) = (K - m_k(\phi)) \ \bigcup \ m_k(\psi)$$ $$m_k(0) = \emptyset$$ $$m_k([\alpha]\psi) = K - (m_k(\alpha) \ o \ (K - m_k(\phi))$$ $$m_k(\alpha;\beta) = m_k(\alpha) \ o \ m_k(\beta)$$ $$m_k(\alpha \ \bigcup \ \beta) = m_k(\alpha) \ \bigcup \ m_k(\beta)$$ $$m_k(\alpha^*) = m_k(\alpha)^* = \bigcup \ m_k(\alpha)^n, where\ n>0$$ $$m_K(\psi?) = ( (u,v) \ | \ u \in m_k(\psi) ) $$ The previous definition can be extended by induction to all formulas and programs.

As Noah Schweber said below: "The point is that the definition of "nonstandard Kripke frame" is the same as the definition of "standard Kripke frame," except that one condition is weakened: rather than having the property that $m_N(\alpha^∗)$ is the reflexive transitive closure of $m_N(\alpha^∗)$ (which is required of standard Kripke frames), a nonstandard Kripke frame merely needs to satisfy the weaker condition."

How can I show that all finite non-standard Kripke frames are standard?

1

There are 1 best solutions below

3
On BEST ANSWER

See pages 199-200 of this book. The point is that the definition of "nonstandard Kripke frame" is the same as the definition of "standard Kripke frame," except that one condition is weakened: rather than having the property that $m_\mathfrak{N}(\alpha^*)$ is the reflexive transitive closure of $m_\mathfrak{N}(\alpha)$ (which is required of standard Kripke frames), a nonstandard Kripke frame merely needs to satisfy the weaker condition $$\mbox{$m_\mathfrak{N}(\alpha^*)$ is a transitive reflexive extension of $m_\mathfrak{N}(\alpha)$ satisfying properties 5.5(vii-viii).}$$ So every standard Kripke frame is a nonstandard Kripke frame, in the same way that every rectangle is a square. (A better name for nonstandard Kripke frames might be "possibly nonstandard Kripke frames" for this reason, but that's a mouthful.)