Propositional Dynamic Logic Compactness

115 Views Asked by At

I know that Propositional Dynamic Logic is NOT compact, but I don't exactly know how to show that. I know that the given set:

$$ \def\<#1>{\langle#1\rangle}\left\{\<a^*>b\right\} \cup \left\{¬b,\;¬\<a>b,\;¬\<a^2>b,\;\ldots\right\} $$

is finitely satisfiable, but not satisfiable. Can anyone help me prove that?

PS: $\<a>$ stand for diamond and $a^n$ says that the program $a$ is iterated $n$ times; here $a$ represents a program and $b$ an assertion.

1

There are 1 best solutions below

0
On BEST ANSWER

$\def\<#1>{\langle#1\rangle}$If you take any finite subset of the $\neg\<a^n>b$ sentences, you can find the maximum $n$ in it. Let it be $m$. Then a model with $m+2$ states exists that satisfies the whole set. If PDL enjoyed compactness, then the whole set would be satisfiable, but it obviously isn't, because a model for the whole set of sentences satisfies $\<a^*>b$, which requires $\<a^\ell>b$ to be true for some $\ell$. Hence compactness does not hold for PDL.