以下のエントリー群で断片的に述べていたことをまとめておきたい -- 「ならば」の論理的解釈とは何だろうか？
記号法
まず記号：
- |= ：充足（satisfies; validity, correctness）
- |- ：証明可能（proves/derives; provability, derivability）
- ⇒ ：内容的含意（implies; conditional implication）
- ⊃ ：含意（implies）
- → ：？
- |⇒ ：伴意、意味的帰結（entails; entailment, semantical consequence）
上の3つ（|=, |-, ⇒）は“地の文”で使うものだから、自然言語表現で代替できる。あえて記号を使うのは：
- 明晰さを増すため、
- 形式化の伏線として。
記号「⊃」は、論理結合子、論理演算記号としての含意だ。古典論理なら、A⊃B は ¬A∨B で置き換えてもよいので、記号「⊃」は不要だともいえる。が、含意記号がないのは気持ち悪い。記号「→」はシーケントの前件（前提）と後件（結論）を区切る記号、なんて読むか知らない。「→」を"entails"という人もいるし、僕もそう読むときもあるが、意味的帰結（上記の記号では「|⇒」）と区別が付かなくなる。「|⇒」は、前提と結論の概念を意味的（モデル論的）な主張（assertion, judgement)として定義したもので、「|=, |-, ⇒」同様、地の文で使うものだ。
なお実際には、記号（特に矢印「→」）をオーバーロードして使うので、ここまで細かく区別はしない（「文字や記号はいつだって足りないのだ」参照）。
「ならば」について
「⊃, →, |⇒」の区別は難しい。とりあえず「⊃」は記号的体系内部で天下りに与えられる結合（演算）記号だと思ったほうがいい。「⊃」の解釈は「ならば」なのだが、それを強調すると、他の記号（概念）との区別がつかなくなる。とりあえずは、A⊃B は ¬A∨B の略記と思うのも手かも知れない。
シーケント計算の「→」はさらに形式的な天下り記号になる。が、理解の仕方としては、‘A1, ..., An → B1, ..., Bm’は‘→A1∧...∧An⊃B1∨...∨Bm’と（形式的計算で）同値であり、単一の論理式‘A1∧...∧An⊃B1∨...∨Bm’と事実上同じだと（内心では）納得しておいたほうがいい。
伴意記号を含む A1, ..., An |⇒B は、意味的・内容的な言明である。「|⇒」の定義にはモデル論を出す必要がある。
- A1, ..., An |⇒B とは、M |= A1, ... M |= An であるモデルMは必ず M |= B でもあること。
普通の内容的含意「⇒」は、モデル論的な伴意のことだろうと思う。つまり、日常的「ならば（⇒）」の精密な定義が「|⇒」だといえる、おそらく。
「ならば」達の関係
「A⇒B」の意味が「A|⇒B」だとすれば、日常的な直観はきわめて超越的なモデル論を無意識に使っていることになる。なぜなら、「条件Aを満たすあらゆるモノ」を考えているのだから。繰り返し言うが、「A|⇒B」の意味は、「条件Aを満たすあらゆるモノは、必然的に条件Bを満たす」だった。
さて、とある演繹系（deduction/proof system）があって、‘A⊃B’が証明できるとする。これは、|- A⊃B と書ける。|- A⊃B が A|⇒B を保証する（つまり、演繹系が健全）なら、|- A⊃B と A|⇒B はだいたい同じことだと言っていいだろう。
演繹系で演繹定理（と呼ばれるメタ定理）が成り立つと、|- A⊃B ⇔ A |- B となる（ここでの「⇔」は“地の文”で使う同値性、以下でも⇔は地の文で使うよ）。つまり、|- A⊃B と A|⇒B と A |- B は、まー同じだと言っていい。演繹定理が成立する演繹系が健全かつ完全だという理想的状況では、次の三つが一致することになる。
- A |⇒ B ： BはAの意味的帰結である（AはBを伴意する）。
- |- A⊃B : 論理式‘A⊃B’が無条件で証明できる。
- A |- B ： Aを仮定して、Bを証明できる。
シーケント計算（ゲンツェン方式演繹系）
‘A→B’の形を持つ式を扱う演繹系があって、記号「||-」がその演繹系での証明可能性を表すとしよう（||- も地の文で使う記号）。この新しい演繹系が以前の演繹系をよくシミュレートしているとする。これは、次を意味する。
- A |- B ⇔ ||- A→B
例えば、A |- B ⇔ |- A⊃B なのだから、||- A→B ⇔ ||- →A⊃B も成立する。シーケント計算とは、まーこういうものだ。となると、シーケント計算における証明可能性である||- A→B もまた「ならば」の表現となる。もう一度まとめると：
- |- A⊃B ： 無条件（仮定なし）の絶対的証明可能性
- A |- B ： 仮定をいれた相対的証明可能性
- A |⇒ B ： 超越的モデル論的な主張、あるいは日常的な「ならば」
- ||- A→B ： シーケント計算の絶対的証明可能性
これらの「ならば」達の関係をハッキリと示すには、演繹定理、健全性／完全性、ヒルベルト式式演繹系とゲンツェン方式演繹系（シーケント計算）の同等性などが必要になる。逆に、これらのモデル論／証明論の基本概念は、「ならば」の諸相を説明するためにある、と考えてもいいだろう。
