最小論理の確率的意味論

はしがき

　GW ということでなにかやりたいなと思い最小論理の確率的意味論を検討していました。もともとの動機はゲーム理論を論理学の知識で拡張できないかというもので、利得関数の計算のために論理式を使おうというところが出発点でした。いろいろと試行錯誤するうち、結果的には確率論のほうが色濃い体系となりそこそこかたちになってきましたのでまとめます。

(2021-05-03)

最小論理について

　最小論理は直観主義論理から爆発律を取り除いた体系です。爆発律は

　という形式の推論です。ただし無矛盾律は含まれます。つまり

　および

　という形式の推論は最小論理でも可能です。

命題と集合の対応関係について

　命題は集合を表すものと見ることもでき、確率論における事象と見るならば、つぎのような対応関係があります。

　論理包含に対応するものは冪乗で定義されており、集合論では冪集合は写像全体の集合を表します。この関係を直観的に説明すると、論理包含と冪乗のあいだにはつぎのような関係があります。

　これによって上記のように確率測度でもって真理値を定義しても最小論理の健全性や完全性を壊さないというものが最初の直観です。

確率的意味論をもつ最小論理の体系

論理式

　V を変数の集合とします。最小論理の論理式すべての集合を U と表し、次のように帰納的に定義します。

　最後の ¬p は単なる p→⊥ の略記です。基本的な構文形式として定義することもありますが、今回は派生形式として定義します。

公理型と推論規則

　証明図を書くための公理型と推論規則を定義します。A が公理型で、それ以外は推論規則です。証明図の書き方については割愛します。

　Γ の部分の波かっこや ∪ という記号（※）と論理式のかっこは “よくある順序で” 適当につけたり省略してもよいものとします。これは証明図を “よくある書き方” で書くための約束です。

　（※）Γ という部分は（この体系では）仮定の有限集合ですが、形式化には流派があります。あくまで集合ではなく記号列とする場合には（厳密には）記号の結合や並び替えに関する規則を定義する必要があります。部分構造論理という体系ではこの部分に関する規則が検討されています。線型論理などが有名です。

　とくに Γ = ∅ のとき Γ ⊢ p を単に ⊢ p と記述します。⊢ p なる証明図が存在するとき p は証明可能であると言います。

真理値

　変数から [0,1] の区間への写像 ν が与えられたとき、命題の真理値 |p| をつぎのように定義します。

命題の真偽

　ある

　が与えられ

　なるとき p を (ν のもとで) 真なる命題と言い

　と表します。

恒真式

　いかなる

　をとっても

　なるとき p を恒真式と言い

　と表します。

健全性と完全性

　健全性とは p が証明可能ならば p が恒真式であることです。

　完全性とは p が恒真式ならば p 証明可能がであることです。

　この体系では完全性はおそらく成り立たないと思われます。排中律がないので、恒真式であるにもかかわらず証明できない命題は無数に考えられます。

　健全性の証明は省略しますが、ここには基本的なアイデアを記しておきます。

　真理値の符号をとれば sgn(ν(x)) ∈ {0, 1} になることから真理値が {0, 1} の値をとる特殊な体系を考えればそれぞれの真理値が二値論理に対応することがわかります。また |p| の定義からそれぞれの命題が 0 の場合と 0 でない場合の場合分けで命題の真偽が保存されることがわかります。

所感

真理値の “意味”

　この体系では（構文論的には）同値な命題でも（意味論的には）真理値が異なる命題というものが存在します。もっとも単純なものでは |A|≠0,1 の場合に |A∧A|≠|A| かつ |A∨A|≠|A| です。この体系を構成しているうちに、おもしろいと思ったものを紹介します。

　⊤ はあまりおもしろくはありませんがあって当然なのでいれました。 |⊤|=1 です。

　A⊼B は排他的論理和の否定 (XNOR) もしくは同値 (EQ) で、ふつうは ⇄ と書かれるものです。この真理値は |A|,|B| ≠ 0 ならば |A⊼B|=|A∧B|, |A|,|B|=0 ならば |A⊼B|=1, そうでなければ|A⊼B|=0 となります。

　A⊻B はいわゆる排他的論理和 (XOR) です。これは構文的には同値 (EQ) の否定に等しいです。|A|≠0 かつ |B|=0 ならば |A⊻B|=|A|, |A|=0 かつ |B|≠0 ならば |A⊻B|=|B|, そうでなければ |A⊻B|=0 です。

否定の極性

　すこしおもしろいと思ったこととして否定は常に {0,1} の真理値をとるということです。つまり |p|=0 ならば |¬p|=1, |p|≠0 ならば |¬p|=0 ということです。最初 |¬p|=1-|p| のような素朴な定義を考えていましたが、そうすると |p|=0.5 とかの否定も |¬p|=0.5 とかになってしまい大変です（※）。

　（※）体系によってはこのようなものが存在します。しかし今回はあくまで最小論理の単純な拡張としたかったことと、この体系を自然に二値論理に埋め込むことができるようにしたかったのでこうしました。実際、この体系に爆発律や排中律を追加して直観主義論理や古典論理に拡張することは可能だと思われます。

対数の真理値

　含意が指数なのであれば対数が真理値となるような論理式は存在するか考えたくなってしまうものです。

　もっとも単純な観察は |p→q|,|q|≠0,1 ならば log_|q|(|p→q|)=|p| だということです。これは仮説形成にも似ています。 |p→q|,|q|=0,1 の場合はそれぞれ二値の真理値として定義できそうです。

測度論との関係

　直観的に真理値の “意味” が想像しやすいので “確率的” としましたが確率空間や測度空間を仮定してはいません。ゲーム理論の利得関数を扱うために使うことも考えられます。このように真理値を確率として扱う必要は必ずしもないので “重みつき” くらいの一般的な名称のほうが適しているかもしれません。ただし ν が測度や確率測度であるようなこの体系の類を考えることはできます。

環への一般化

　真理値の定義中で除算を使用していないので、実際のところ（実数などではなく）環であればよい可能性はあります。もちろんその場合真理値の “意味” は変わることになりますが、構文的にはそのように拡張できる余地はあります。

　実際定義を見ると集合環の定義に似ている部分がいくつかあります。とくに対称差は和事象の確率によく似ています。

おわりに

　今回は真理値をこのように定義しても（おそらく）最小論理の壊さないだろうというところまで確かめられました。ν:V→[0,1] を ν:V→{0,1} とすればもともとの二値論理と同じ真理値表がつくれ、自然な拡張になっているということが大事です。

　ほんとうはこの真理値表を使って利得関数を定義したり、より発展的なことをしたいわけですがこれだけでもだいぶ時間がかかってしまいました。いろいろとおもしろい話ができそうだと思っていたのですが、まずは第一歩ということで今回は最小論理の真理値にこのような重みづけをするまでとします。

　現段階でも論理体系としてそこそこ使えるものにはなっていると思います。今後は制約充足問題、ゲーム理論などへの応用などを検討しています。

　より興味のあるかたのために、付録に体系の定義を掲載します。どうぞご覧ください。