Vtyjkyuk

Prove that PDL (Propositional Dynamic Logic) is compact over nonstandard models. That is, every finitely satisfiable set of propositions is satisfiable in a nonstandard Kripke frame. Conclude that there exists a nonstandard Kripke frame that is not standard.

You can find nonstandard Kripke Frame definition here.

I bumped into this problem inside the book called "Dynamic Logic" by Harel, Kozen and Tiuryn. It is exercise 7.3 from the book. I have no idea how to approach it.

I assume you have access to the book you mention.

In chapter 7, right after lemma 7.2 a nonstandard model $mathfrakN$ is constructed, whose points are the maximal sets of consistent formulas. It's not hard to see that the Truth Lemma holds for this model, i.e. $smodelsvarphi$ if and only if $varphiin s$(the proof is similar to the proof of the truth lemma for standard modal logic, for the non trivial part see e.g. Existence Lemma 4.20 in Modal Logic by Blackburn et al.; maybe in the book you mention this is also shown but I didn't check). This model is the canonical (nonstandard) model of the logic given in the beginning of chapter 7.

Now let $Sigma$ be a set of finitely satisfiable formulas. By soundness any finite set of formulas that is satisfiable is consistent. Therefore every finite subset of $Sigma$ is consistent. Since the proof system given is finitary (i.e. proofs are finite) this means that $Sigma$ is consistent. Therefore it can be extended in a maximal consistent set of formulas $Sigma'$. $Sigma'$ is a point in $mathfrakN$ and by the truth lemma mentioned above $Sigma'$ satisfies all the formulas of $Sigma$, i.e. $Sigma$ is satisfiable.

Now since PDL is not compact with respect to standard models (the set $$langle a^astrangle p,lnot p,lnotlangle arangle p,lnotlangle aranglelangle arangle pldots$$ is usually used as to show this) it follows that $mathfrakN$ is indeed not standard.