様相論理の公理4
$ \square A \models \square \square A
任意フレーム$ F=\langle W,R \rangleについて
$ \square A \models^F \square \square A
証明
$ \impliedby
まあ自明ということで
$ \implies
任意フレーム$ F=\langle W,R \rangleについて$ \square A \models^F \square \square Aならば$ Rが推移的
対偶を取る
任意のフレーム$ F = \langle W,R\rangleで$ Rが推移的でないなら$ \square A \not\models^F \square\square A
そういう論理式$ Aを一例だけ持ってこればよいので単に要素命題$ pとして
任意のフレーム$ F = \langle W,R\rangleで$ Rが推移的でないなら$ \square p \not\models^F \square\square p
反例の定義に従って
任意のフレーム$ F = \langle W,R\rangleで$ Rが推移的でないなら
$ F上の付値$ vと$ x \in Wについて
$ v(x,\square p) = 1
$ v(x,\square\square p) = 0
$ xRy,yRzだが$ xRzでない$ x,y,z \in Wが存在する
付値$ vを任意の$ w \in Wについて
$ v(w,p)=1 \iff xRwと定義する
$ xRwなら$ v(w,p)=1なので$ v(x,\square p) = 1
https://gyazo.com/0ae2074cd0c793815ba70494881a5658
これより，$ Rが推移的でないどのようなフレームにもその上に反例モデルを構築することが出来ることが示された
対偶を示した
したがって任意のフレーム$ Fで$ \square A \models^F \square\square Aなら$ Rが推移的