risk = nil;

論理は，他の形式的なシステムと同様に，次の3つのコンポーネントから成り立っている．構文・意味・証明論である（p.146）

• 構文は，文法に合った文を定義するための一連の規則である

• 意味は，文の正確な意味を定義するための一連の規則である

• 証明は，既存の文から新しい文を導出するための，一連の導出規則 ¹である．

命題論理

最初の例は，以下である．

trainMoving → doorsClosed

多くの人は，「列車が動いているならば，ドアは閉まっている」と考えるに違いない．文の魅力は「省略」にあると思っているが（俳句が典型的な例），それは人が読み取ろうとする力を惹起するからと思っている．

さて，4.4節は，基本的に原書に従うが，規則中心にはしないつもりである．論理学の日本語の教科書としては，「論理学をつくる」というすばらしい入門書がある ²．「つくる」ということばがとても良い．あるいは，D.グリースの「プログラミングの科学」がある ³.

さて，命題論理では，trainMoving を以下に変えても全く差し支えがない．即ち，命題論理の世界では，原子式（単純命題）の中身を読み取ってはいけない．

1. 列車は動いている，
2. P
3. trainStopped

記号の中身は問わない．∧（かつ）や ∨（または）といった演算子による記号の操作である．現実の我々の考え方に関係はしているが，基礎づけられているわけではない．似ている点があったとしても，現実世界とは別に成立しているのである．分かりづらさがあるとすれば，どっちつかずに見える点かもしれない．

先の式は，よく知られているように次のように変形できる．

¬trainMoving ∨ doorsClosed

→（含意，条件法）は，扱いにくいので，この変形が行われる．最初だけ真理値表で確認しておこう．

典型的なトートロジーと呼ばれる変形である．

よく知られているように，→は，前件（条件部）がF（偽）ならば，後件の真偽にかかわらずT（真）である．前述のように，そういう規則と割り切っておかないといけない（なお，この点については再度触れることにする）．

「Cの場合は，Aを実行します」と仕様書に書いてあったとする．¬Cの場合に，異常なふるまいをしたときに，それは仕様外ですといえるかどうかは，ケースバイケースである．プログラミングであれば，防衛的にすべきという標語が相当するか．

（nil）