様相論理のメモ。S5フレームは、KTB4ともKT5とも特徴づけられるが、KDB4とかKDB5とも特徴づけられる。とりあえず、ここでは
- T:□φ→φ
をKDB4から導出してみる。
□φと¬φを仮定する。Bにより¬φ→□◇¬φ。Dにより□◇¬φ→◇◇¬φ。4により◇◇¬φ→◇¬φ。定義により◇¬φ ≡ ¬□φ。¬□φは仮定の□φと矛盾するので、φ。よって□φ→φ。
様相論理のメモ。S5フレームは、KTB4ともKT5とも特徴づけられるが、KDB4とかKDB5とも特徴づけられる。とりあえず、ここでは
をKDB4から導出してみる。
□φと¬φを仮定する。Bにより¬φ→□◇¬φ。Dにより□◇¬φ→◇◇¬φ。4により◇◇¬φ→◇¬φ。定義により◇¬φ ≡ ¬□φ。¬□φは仮定の□φと矛盾するので、φ。よって□φ→φ。