どんな分野でも、用語法や記号法の不整合はあるでしょう。歴史的な経緯でしょうがないのですけど、それが学習者を混乱させたり大きな障害になったりします。僕は、このテの問題に悩まされることが多いので、このダイアリーでもけっこう話題にしています。
んで、今日は、証明可能性を表す記号「|-」（ターンスタイル）と普遍妥当性を表す記号「|=」（ダブルターンスタイル）をまた*1取り上げます。
論理システムが健全であることを、普通次のように述べます。
- どんな論理式Aに対しても、|- A ならば |= A
このような「|-」、「|=」の使い方はよく見かけます。が、「|-」と「|=」の使い方／意味って、なんか対称性が欠けるよなー、と思います。「|=」とは別な記号、例えば「|⇒」を使って、
- どんな論理式Aに対しても、|- A ならば |⇒ A
のように書いたほうが整合的な気がします。以下に理由を書きましょう。
関係記号としての「|-」と「|=」の意味
論理システムSがあって、これは演繹系（証明系）もモデル（意味論）も備えているとします。Sの演繹系による証明可能性を |-S と書きます。モデルに関する充足（満足、充当）関係（satisfaction relation）を |=S と書きます。これは普通通りです。下付き添字のSは省略することもあります。
Sの論理文（閉じた論理式）の全体をSen(S)、Sのモデルの全体をMod(S)とします。この記法はインスティチューションに倣いましたが、インスティチューションは出てきません。
「|- A」という書き方のAを変数だと思うと、次の集合Provableが定義でます。
- Provable = {A∈Sen(S) | |-S A}
左側がカラッポの「|-」の意味は、Sen(S)の部分集合だと言っていいでしょう。しかし、「A |- B」のような書き方もあります。これは、Aを仮定すればBが証明できる、という相対的証明可能性です。「A |- B」のA, Bを変数だと思うと：
- RelProvable = {(A, B)∈Sen(S)×Sen(S) | A |-S B}
と、Sen(S)×Sen(S) の部分集合が定義できます。そして、「|- A」と「A |- B」の関係は：
- |- A ⇔ true |- A
結局、記号「|-」の意味は Sen(S)×Sen(S) の部分集合だと思えばいいことになります。
次は「|=」。「|=」では、左にモデル、右に文を置きます。ですから、「|=」を外延化した集合は次のようになります。
- Satisfaction = {(M, A)∈Mod(S)×Sen(S) | M |=S A}
記号「|=」の意味は Mod(S)×Sen(S) の部分集合です。
単項述語記号としての「|-」と「|=」の意味
左がカラッポの「|-」の意味は既に定義しました。真を表す記号true（特殊な文と考える）を使って次のように定義できます。
- |- A ⇔ true |- A
左がカラッポの「|=」の意味は次のとおりです。
- |= A ⇔ 任意のM∈Mod(S)に対して、M |= A
「|-」と「|=」は似た記号ですが、左辺を省略したときの扱いが全然違います。この点がどうも歪んでいるように感じます。もちろん、「そういうもんだ」と割り切ればいいのですけどね。
新しい関係記号「|⇒」
意味論的な関係記号「|⇒」を次のように定義します。ここに出てくる記号「⇔」は地の文で使っている内容的な同値関係ですから注意してください。
- A |⇒ B ⇔ (任意のM∈Mod(S)に対して、M |= A ならば M |= B)
この関係 |⇒ は、|= を基にして定義されるので意味論的です。しかし、記号「|⇒」の左も右も文なので、Sen(S)×Sen(S) の部分集合として意味を持ちます。そして、左辺の省略は次のように定義できます。
- |⇒ A ⇔ true |⇒ A
M |= true は、Mが何でも成立するので、|⇒ A は次のことを表します。
- |⇒ A ⇔ 任意のM∈Mod(S)に対して、M |= A
そういうわけで、健全性の表明は次のように書くのがよかろうと思うわけです。
- どんな論理式Aに対しても、|- A ならば |⇒ A
記号「|⇒」を使えば、推論規則の妥当性の記述も簡単になります。Sの演繹系が次の推論図を許すとしましょう。
A
-------
B
この推論図（推論規則）が意味論的に妥当であることは、次のように書けます。
- 任意のMに対して、M |= A ならば M |= B
これは、A |⇒ B のことです。つまり、推論規則としての A |- B （Aを仮定すればBが出る）が妥当であることを、A |⇒ B だと言えます。A |⇒ B が保証されているなら、次が言えます。
- |⇒A ならば |⇒B
ところで、「A |- B ならば A |⇒ B」という主張は、形の上で健全性の主張に出てくる「|- A ならば |⇒ A」と似ています。推論規則が意味論的に保証されることも「健全」と呼ぶほうが一貫性があるかも知れませんね。
さらに言葉と記号の問題
M |= A という関係は、充足とか妥当とか呼ばれるのですが、主語・述語をどう使うか僕はよくわかりません。「M(主語はモデル)は、Aを充足する」、「A(主語は文)は、Mに対して妥当である」と言うのだと思いますが、自信がありません。「Aが普遍妥当式である」という用法があるのは確実で、これは「任意のMに対して M |= A」のことです。
「充足」がモデルに関する記述、「妥当」が文（論理式）に関する記述に使われるようですが、「Aが充足可能だ」とは「あるMに対して、M |= A」という意味みたいです。「Mが充足可能だ」は、「あるAに対して、M |= A」かな？ -- 聞いたことないけど。
|-S A を S|- A と書く人／ときもあるようです。この書き方だと、相対的証明可能性を表すために、別な記号（例えば、|>）を導入して、S|- A |> B のように書く必要があります。|=S を S|= と書くのは見たことないです、あるのかな？（[追記]M |=S A を S|=M A と書くのはあるかもな、なんとなくそんな気がするだけで、事例は出せませんけど。Aに自由変数があるとき、σを値割り当てとして、M |=σ A って書き方は見たことあります。これは、M, σ |=S A って書き方もあったような、、、アーきりがない。[/追記]）
まー、そんなこんなで、言葉と記号の用法は混乱しているので、ご注意くださいってことですね。
*1:同じ話題を過去にも取り上げたことがあります。面倒なので参照リンクは示しませんが。
