0
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ @hardmath I hope that I edited it so everyone can understand the question. Please let me know if not. $\endgroup$ – theSongbird Jan 9 '17 at 6:47
  • $\begingroup$ I'm sorry, but I think I don't get the question. Should I expand the context even more? $\endgroup$ – theSongbird Jan 9 '17 at 15:58
  • $\begingroup$ I'm asking (to put it by analogy) if you meant to ask if every square is a rectangle, or if every rectangle is a square? See how you phrased your title and final sentence of Question. Compare this to what Noah wrote. $\endgroup$ – hardmath Jan 9 '17 at 16:01
  • 1
    $\begingroup$ Thanks a lot, mate. I changed the question a bit. Following our analogy with squares and rectangles I could say that I want to prove that "all rectangles with a specific property are squares" (we norrow the meaning "property" adjective a lot). $\endgroup$ – theSongbird Jan 9 '17 at 16:11
  • $\begingroup$ The Question here is Exercise 6.5 (pg. 202) in Dynamic Logic, the same book linked to by Noah Schweber. $\endgroup$ – hardmath Mar 10 '17 at 15:46
1
$\begingroup$

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.)

$\endgroup$
  • $\begingroup$ perhaps you mean "in the same way that every square is a rectangle"? $\endgroup$ – nomadreid Jan 9 '17 at 6:12
  • $\begingroup$ I'm sorry , but thank to hardmath's feedback , I realised I had to change the question a little. Does this answer still stand? (no irony intended) $\endgroup$ – theSongbird Jan 9 '17 at 16:09
  • $\begingroup$ Hmm a better name might be "general Kripke frame" so that "nonstandard" can be used for those that are not "standard"? $\endgroup$ – user21820 Jan 14 '17 at 6:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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