一階述語条件論理とそのタブローシステム
理学専攻 情報科学コース 尾崎有梨

1

はじめに

形式意味論では、自然言語の文の意味を論理式を用いて表す。その中でも条件文は未解決であるが重要な構文のひとつであり、これまでにも解決法として様々なアプローチがなされてきた。
例えば、古典論理では次のような推論が成り立っている。
前件強化 A ⊃ B  (A ∧ C) ⊃ B
推移律 A ⊃ B, B ⊃ C  A ⊃ C
対偶 A ⊃ B  ¬B ⊃ ¬A
しかし、古典論理を自然言語の意味論として考えたとき、上の三つに相当する例文の中には、次のような不適切な推論が含まれる。[6, p.82](1) If it does not rain tomorrow we will go to thecriket. Hence, if it does not rain tomorrow and I
am killed in a car accident tonight then we will
go to the criket.
(2) If the other cadndidates pull out, John will getthe job. If John gets the job, the other candidates will be disappointed. Hence, if the othercandidates pull out, they will be disappointed.
(3) If we take the car then it won’t break down
en route. Hence, if the car does break down enroute, we didn’t take it.
この不適切さの理由は、条件文を述べるときには、明らかな前提は省略するということにある。例えば、(1)の１文目では「雨が降らない」ことを仮定しているが、その時は明日事故で死ぬかもしれないということは通常考えず、事故で死なないということを当たり前の前提として話が進められる。しかし (1) の 2 文目では、当たり前のこととして省略されている前提に反する事象を述べてしまっているため誤った帰結が導かれてしまっている。
(2) と (3) も同様に、前提部分の条件に暗黙に含まれているものが省略されていて、(2) の場合、２文目の本来の意図は “if John gets the job and the other candidates
do not pull out, they will be disappointed.” である。
“we take the car” という前提が省略されているにも関わらず、“we didn’t take it” と述べているために意味の通らない文となっている。
このように、古典論理に基づく意味論では、自然言語の条件文を適切に表すことができないことが知られている。そこで本研究では、自然言語の条件文を適切に表す論理体系を構築することを目的とする。

2条件論理
1 節の (1) の例文の問題を解決するものとして、前提としては省略されるべき当たり前のことという概念、ceteris paribus を論理体系に取り入れるということがあげられる。条件文はなにかしら ceteris paribus の概念を含んでいると考えられていて、この概念を含意の定義に含めた体系である「条件論理 (Conditional Logic)」(指導教員：戸次大介)が様相論理の一種として体系化された。[4]条 件 論 理 の ク リ プ キ フ レ ー ム は W, {RA : A ∈F}, ν の 3 つ 組 で あ る 。W と ν は 様 相 論 理 の 時と同じように、それぞれ、空でない世界の集合、世界 w の 集 合 と 命 題 記 号 p において真偽を表す関数
νw (p) = 1(又は νw (p) = 0) である。各 RA は W 上での二項関係を表す。任意の式 A において、w1 RA w2と は 、w2 は A が 真 で あ る 他 は w1 と 変 わ ら な い(ceteris paribus) という意味である。さらに、条件論理
では ceteris paribus を含んだ論理体系のために新しい論理記号 > が追加される。> は二項述語で、真理条件は

ν(A > B) = 1 ⇐⇒wRA w となる全ての w において、νw (B) = 1 になる。となる。
また、以下のような概念 fA (w)、[A] も追加される。

• fA (w) = {x ∈ W : wRA x}• [A] = {w : νw (A) = 1}
fA (w) は RA のもとで w からアクセス可能な世界の集合のことで、また、wRA w ⇔ w ∈ fA (w) なので Rと fA (w) は相互的に定義可能である。[A] とは A が真となる世界 {w : νw (A) = 1} の集合である。
さらに、自然言語に適切に対応するために、条件論理の拡張 C + では以下の条件を加えることによって定義した。[2]1.
2.

fA (w) ⊆ [A]もし w ∈ [A] なら、 w ∈ fA (w)3

V Cb (CI)

条件論理では当たり前の前提を省略できるようになったが、条件文の前提に置けるものが限定されているため依然として十分に自然言語の条件文を適切に表せているとは言えない。また、拡張されたものの中には推論の妥当性の証明がモデル理論的にしかできないものもあり、後にプログラミング言語との対応など応用することを考慮にいれると、アルゴリズム的に証明できる体系が必要となる。そこで条件論理からさらに拡張した論理体系を構築する。拡張する上で本研究で特に着目した点は以下の 4 点である。

i 一階述語論理にする
ii 同一性を表現できるようにする
iii タブローで証明できる [5]iv 世界間の移動がより可能にできるようにする
i) と ii) については、より自然言語に対応した論理体系に存在することが当然望ましい。iii) のタブローとは恒真式を判定する証明アルゴリズムで分析を行いやすくする。iv) は一階述語条件論理にするにあたり、現実の世界と架空の世界との区別に必要となる。次節でこれらを満たした新しい体系 V Cb (CI) の定義を行う。

3.1

統語論 · 意味論

V Cb (CI) の統語論は以下のようになる。

∃x(p(x) ∧ q(x)) > r, 0p(a) > q(a), 0¬(p(a) > r), 0↓0rp(a) 1p(a), 1¬r, 1↓q(a), 1¬q(a), 1q(a), 1×1rq(a) 1↓0rp(a)∧q(a) 1↓0r∃x(p(x)∧q(x)) 1↓r, 1×F ::=p | ¬F | F ∧ F | F ∨ F | F → F | F ⊃ F | F ↔ F| 2F | 3F | F > F | ∀xF | ∃xF |τ = τ | E
τ ::=c | xi) を解決するために一階述語論理として可変領域(Variable Domain)[1] という概念を、ii) を解決するた
めに偶発的同一性 (Contingent Identity)[3] を採用した。可変領域からは、非実在のものについても述べるために存在述語 E も導入されている。存在述語では Ea
で「a が存在する」という意味を表す。
ま た 、V Cb (CI) の ク リ プ キ フ レ ー ム は
D, W, H, {RA : A ∈ F}, ν の 五 つ 組 で あ る 。
W と R については条件論理の時と同じである。H は、avatar と呼ばれるオブジェクトの集合である。D は全てのオブジェクトの集合で空でない領域であるが、Wから H への関数を要素とする。存在述語については
νw (E) = Dw と定義する。自由変数 x が現れるようになったことから新たな記述も追加される。Ax (c) とは式 A の中の自由変数 x を定数 c に置き換えるという意味である。また、領域の全ての要素 d について、
ν(kd ) = d となるような定数 kd が存在するとする。これにより、量化記号条件記号の真理条件は以下のようになる。

• νw (∃xA) = 1 ⇐⇒ ある d ∈ Dw において、
νw (Ax (kd )) = 1• νw (∀xA) = 1 ⇐⇒ 全ての d ∈ Dw において、
νw (Ax (kd )) = 1• νw (A > B) = 1 ⇐⇒ fA (w) ⊆ [B]
また、新たに ADC(Accessibiolity Denotation Constraint) と呼ばれる条件が追加される。

3.

もし ν(a) = ν(b) なら、RAx (a) = RAx (b)3.2

新規則の追加これまでの論理体系の共通の問題の一つとして、到達可能性 R の条件部分に ∧ や ∨ などが現れるとき、すなわちこれらの真理関数が条件論理の前件部にある時に対応できず、これらを含む推論は全て成り立たなくなっていた。そこで以下の条件をクリプキフレームに加えることによって、C + の拡張でタブローで証明できるという性質を保ちつつ、同時に現存の推論を妥当にすることを可能にした。[5]4.
5.

w ∈fA (w) fb (w ) ⊆ fA∧B (w)fA (w) ⊆ fA∨B (w)fB (w) ⊆ fA∨B (w)さらに、存在量化の条件付きの到達可能性についても同じように推論を妥当にする規則を追加した。[7]6.

fp(a) (w) ⊆ f∃xp(x) (w)

これらは iv) の解決にもつながる。
新たに提案した V Cb (CI) が論理的に妥当であるには、健全性と完全性が成り立つことを証明する必要がある。[8] ではその証明も行い、V Cb (CI) が自然言語により適した論理体系というだけでなく、論理体系として妥当であることを証明した。

4

検証

V Cb (CI) でどのような推論が妥当であるか簡単な例をあげる。
例 1) ∃x(p(x) ∧ q(x)) > r, p(a) > q(a) V Cb (CI) p(a) > r

5 行目で得られた 0rp(a) 1 と 10 行目の 1rq(a) 1 から、4. のタブローの規則より 0rp(a)∧q(a) 1 を導出できる。
さらに、存在量化に関する到達可能性の規則により0r∃x(p(x)∧q(x)) 1 を得ることができるので、∃x(p(x) ∧q(x)) > r に規則が適用できるようになりタブローが閉じる。またこの推論は、「速度計算が出来る人かつ割合の計算が出来る人なら問題が解決する。a さんは速度計算ができるなら割合の計算はできる」⇒「a さんが速度計算ができたら問題が解決する。」というような例文がつくれる。

5

まとめと今後の課題

本研究では、自然言語の条件文を適切に表す論理体系構築を目的とし、一階述語条件論理に拡張した。到達可能性に関する新たな規則も追加し、論理体系 V Cb (CI)を構築した。V Cb (CI) では可変領域や偶発的同一性にCb 特有の到達可能性の規則を加えたことにより、幅の広い自然言語の表現が可能となった。
また iv) の問題の一部として、現実世界と架空世界の区別など、普遍的な問題の考察の必要がある課題もある。しかしそのような検証のためにも、証明が機械的にでき、その過程も分かりやすいタブローで証明ができるようにしたことは本研究の一つの成果と言える。

参考文献[1] Barcan, R. A functional calculus based on strict
implication. Journal of Symbolic Logic, Vol. 11,pp. 1–16, 1946.
[2] Chellas, Brian F. Basic conditional logic. Journalof Philosophical Logic, Vol. 4, pp. 53–133, 1980.
[3] Kanger, S. The morning star paradox, 1957.
[4] K. Lewis, David. Counterfactuals. Oxford, Blackwell, 1973.
[5] Ozaki, Y. and Bekki, D. Conditional logic Cb andits tableau system. In Logical Aspects of Computational Linguistics, pp. 190–204, 2011.
[6] Priest, Graham. An Introduction to Non-ClassicalLogic. Cambridge Uniersity Press, 2008.
[7] 尾崎・戸次. 一階述語条件論理とそのタブローシス
テム (投稿中). In Programming and Programming
Languages, 2012.
[8] 尾崎有梨. 一階述語条件論理とそのタブローシステ
ム, 修士論文, お茶の水女子大学, 2012.