【検証論】5 ホーア論理の数学 （その6）

最弱前条件がわからない理由がわかった。

 - わかった。そもそも表明の強い弱いのちゃんとした
   定義がこの本でなされていないのだ。だから弱いの
   かどうかがわからないのだ。この文脈からすると、
   弱いの定義は、

   「A => Bのとき、BがAより弱いと言う」

   ということだろう。

これならば、pwp(P,B)が最弱であることは自明。


次回は相対完全性定理。
こつこつ。