論理モデル

プログラムとは論理式だ！

論理式の証明とは計算だ！

論理式自体は値ではない

名前の通り、式だ

式の意味の解釈の仕方を定めて初めて値が定まる

解釈の仕方は無限にある

そもそも現実世界の問題を、証明するために、計算に落とし込むのがそもそもムズイ

証明のスタート地点に立つのがムズイという意味

無限の可能性を論理式で扱うために、扱う論理式を制限する

公理の下で命題が成り立つことを証明する過程が計算に当たる

公理とはHorn節のことで、プログラムのこと

命題とは、データのこと