記号論理学（放送大学）

 放送大学で記号論理学の集中講義があったので学んでみた。

第４回　言語L　M＝｛U,v｝というモデル　個体変項　閉じた式　などについて
　　M⊦　B→C　　⇔　　M⊬　B　と　M⊦C　のいずれか成立
第５回　　A→B　　AがTrueだが、BがFalseである（反例）ものが存在しないとき　正しい
　反例ないことを示すとよい。　反例が１個でもあればだめであるといえる。
　反例が存在すると仮定して、前提をTrue　結論をFalse　とおく
　２５：１０　∀ｘ(Tx→Ｓ'xa）　⊩　￢Ta　　の妥当性　
　　すべてのｘについて　ｘが三角形なら　ｘはaより小さい　そのとき、aは三角形でない
　　aが三角形だとすると、　ｘが丸か五角形でFalse　であれば　左はTrue
　　　　　　　　　　　　　xが三角形なら　ｘ＜a　である必要あるが、ｘがaの可能性ある
　　　したがって、False 矛盾　よって　妥当
　　２８：０８　A→C,B→C　⊦　（AVB）→C　の妥当性
　　　　（AVB）→C　がFalseだとすると　　AVBがTrue かつ　CがFalse
　　　AVBがTrueならば  AかBがTrueでCはFalse
         　よってAがTrue C Falseなら  A→CはFalse　　よって　AはTrueでありえない
　　　　　　　BがTrue　C　False　なら　B→Cは　False　よって　BはTrueでありえない
　　　　よって　AVBはFalse　よって　仮定はあやまりで、結論はFalseではありえない
　　　　となり、反例は存在しないとわかる　よって妥当   

　※とりあえず、書いてみたが、まだ、十分理解してないところもありそう

第６回以降は、タブローという証明支援ツールを実際に使って（サイト上にも自由に使えるアプリがあり非常に便利です）前提⊩結論　が正しいかどうか判定できます。機械的に変形していくだけで、結果がわかるというのが、なかなか素晴らしい！と思いました。

講義もとても丁寧なので、基本を理解するには書籍等で学習するよりスムーズです。

タブローを使っていると以前Coqを使ったのを思い出します。Coqより使いやすいようです。

記号論理学は、プログラミングの論理で混乱したときは、役立ちそうです。