書きかけ記事のリストが長くなるばっかり……（マズイ）。書きかけをローカルディスクに溜め込むよりは、日記エントリにメモを書いておいたほうがいいのかな？
で、ちょっと論理（logic）っぽい話をします。ほとんど小咄です。
「A ならば B」というときの「ならば」に対する定式化が、論理ではやたらにイッパイでてきます。列挙しましょう（これでも一部）：
- → ： 含意（implies）
- |- ： 証明可能（can prove, can derive）
- |= ： 充足（satisfies）
- ⇒ ： 伴意(entails)
記号はとりあえず互いに区別できればいい、というだけで、標準的な記法かどうかは気にしてません。
まず、命題論理（propositional logic）の段階で登場する含意＜がんい＞A→B。これがわからない。A→Bは ￢A∨B（not A or B）と同じだと教わるのですが、納得いかんでしょ、たいてい。「A ならば B」を￢A∨Bだと思っている人なんて、いるのでしょうかね？
A→Bに対する違和感はとりあえず置いとくとして、適当な演繹＜えんえき＞系（証明系；deductive/deduction/proof system）を考えると、メタな命題として 「Aを仮定してBが証明できるなら、A→Bは仮定なしで証明できる」とその逆が成立することがあります。これを演繹定理と呼びます。
記号「|-」は、「左側を仮定して右側が証明できる」というメタな議論（証明論）で使う記号です。この記号を使えば、演繹定理（というメタ定理）は「A |- B ならば |- A→B」とその逆と書けます。どんな演繹系でも演繹定理が成り立つわけではありませんが、我々がよく使う演繹系ではOKでしょう、だいたい。
記号「|=」は、やはりメタな言明のための記号ですが、証明論ではなくてモデル論の記号です。モデルMと論理式Aに対して、M |= A とは、Mが命題Aを真にすることです。Mは条件Aを満たす（M satisfies A）といっても同じ。
最後の伴意＜ばんい＞とは、次のようなことです： M |= A であるようなモデルMに対しては、必ず M |= B であるとき、A ⇒ B と書きます。この定義からわかるように、記号「⇒」もモデル論的なものであり、しかも、やたらに超越的（人間の作業では確認できない／しにくい）ものです。
僕は、日常的な「ならば」は伴意だと思うのですよ。つまり、僕らは、モデル論的・超越的な感覚を最初から持っているような気がするのです。
