一般化量化子を含む自然論理に対する依存型意味論の完全性
理学専攻 情報科学コース 中野 悠紀
はじめに

1

2

Constructive Generalized Quantifiers

Sundholm 1989 で は 構 成 的 型 理 論 (Martin-Löf1984) の枠組みで一般化量化子 (以下 GQ) “most” を定義することで、次のような文において proportion problem の発生を避ける方法を提案した。
(1) Most men who own a donkey beat it.
一 方 、Tanaka & Nakano & Bekki [3] は Sundholm 1989 で 定 義 さ れ た Constructive Generalized
Quantiﬁers が抱える以下の三つの問題点を指摘した。
1. proportion problem が避けられていない
2.

自然論理

3

自然論理は可能な推論とは何かということに焦点を当て、できるだけ自然言語の表面の形を保つ推論を行うことで、推論が自然言語の表面形でどのように直接為されるのかを調べる。依存型意味論 [1] (Dependent
Type Semantics, DTS) は、Polymorphic Dependent
Type Theory (PDTT)(Jacobs 1999) に基づいた自然言語の証明論的意味論の一つである。1) 動的であること、 2) 証明論的であること、 3) 構成的であること、 4)到達可能性が説明できることが主な特徴として挙げられる。これらの特徴により、他の意味論では困難であった言語現象の統一的分析が可能となっている。
本研究では自然論理と依存型意味論の関係を分析するために、一般化量化子を含む自然論理に対して依存型意味論が完全であることを示す。

storong interpretation に関する説明がない

3. uniform ではない
これらの問題に対し、以下のように新しく GQ “most”を定義することでその解決策を示している。この定義
は PDTT に基づいており、この定義の M (k) や [ ] はSundholm 1989 同様の方法で PDTT の枠組みにおいて与えられる。
most の定義 (weak reading)

自然論理は Lakoﬀ1970 で提唱され、80 年代に monotonicity や conservativity 等の性質が自然言語でどのように直接説明できるのかについて van Benthem 1986,
1987 等で研究された。自然論理では可能な推論とは何かということに焦点を当て、できるだけ自然言語の表面の形を保つ推論を行うことで、一階述語論理より簡単なsyntax を与えている。特に Moss は真理条件的意味論とは別のアプローチで推論の研究をするシステムを提案している。 Moss [2] では三段論法の断片に関して推論規則を定義し、その完全性を示している。また基本的な三段論法のシステムに “there are at least as many
A as B” や “Most A are B” などの断片の表現を追加し、その完全性を示すことで、より豊かな表現ができるシステムを提案した。以下では Moss [2] の詳細を紹介したい。
統 語 論: A, B, . . . は 名 詞 の 複 数 形 を 表 す 変 数 の 集
合,J, S, . . . は name をあらわすとして、次の制限された form の文 S について考える。
All A are B

M ost A Bdef≡

Some A are B

N o A are B

J is an A

J is S

M ost A are B

断片:L(all) は All だけをもつ断片を指し,L(all, some, names) は All, Some, names を持つ断片を指す。
意味論:ある model M は集合 M とする。変数各々に対して、A ⊆ M 、name 各々に関してある要素 J ∈ M である。また A が空であることを許すと、All A are B はvacuously に呼び出される。Γ が文の有限または無限集
合ならば M |= Γ は全ての S ∈ Γ について M |= S である。
M |= All A are B

iﬀ

M |= Some A are B

iﬀ

A ∩ B ̸= ∅M |= N o A are B

iﬀ

A∩B =∅

M |= J is an A

iﬀ

J ∈A

iﬀ

J ≡SM |= M ost A are B

iﬀ|A ∩ B| > 1/2|A|(1)

All A are A(2)

All A are C All C are B
All A are B(3)

Some A are B
Some A are A(4)

All B are C Some A are B
Some C are A(5)

J is J(6)

J is S S is F
F is J(7)

J is an A J is a B
Some A are B(8)All A are B J is an A
J is a B(9)

M is an A J is M
J is an A(10)

All A are C N o C are B
N o B are A(11)N o A are A
N o A are B(12)

N o A are A
All A are B(13)some A are B N o A are B
S

L(all, some, no, names) の推論規則(λδ : type)(λc : δ)(Σk : N)
π (sel|(Σx:Entity)Axδc|≥1 (c))+1]+12(k ≥ [ 1∧(Σf : M (k) → (Σx : Entity)Axδc)(f is an A-injection∧(Πy : M (k))(B(π1 (f y))(δ ∧ (Σx : Entity)Axδc)(c, f y)))): (Πδ : type)(Πc : δ)type

さらに証明論では推論が比較的簡単に行えるという利点を活かして、GQ をとりまく様々な言語的性質についても証明可能であることを示している。このように
Tanaka & Nakano & Bekki [3] の形式化では Sundholm 1989 より広い自然言語の empirical coverage を持ち、モデル論的なアプローチの代替としての可能性を示した。

A⊆B

M |= J is S

A : (Πx : Entity)(Πδ : type)(Πc : δ)type
B : (Πx : Entity)(Πδ : type)(Πc : δ)type(指導教官：戸次 大介)

(ΣE∗)(ΣE∗)(ΠE)

m : M ost A are B
m : M ost A are B
π1 (π2 (π2 (m))) : M (π1 (m)) → (Σx : E)Axδca : M (π1 (m))π1 (π2 (π2 (m))) a : (Σx : E)Axδcπ2 (π2 (π2 (π2 (m)))) :m : M ost A are B(Πy : M (π1 (m)))(B(π1 (π1 (π2 (π2 (m)))y))m : M ostA are B
a : M (π1 (m))(δ ∧ (Σx : E)Axδc)(c, π1 (π2 (π2 (m)))y))(ΠE)

π2 (π2 (π2 (π2 (m)))) a : B(π1 (π1 (π2 (π2 (m))) a))(δ ∧ (Σx : E)Axδc)(c, π1 (π2 (π2 (m))) a)(π1 (π2 (π2 (m))) a, π2 (π2 (π2 (π2 (m)))) a) : (Σu : (Σx : E)Axδc)B(π1 u)(δ ∧ (Σx : E)Axδc)(c, u)

(ΣI)

証明 1

L(most, some) の推論規則*14(1)’M ost A are B
Some A are B(3)’

M ost A are B M ost A are C
Some B are C(4)’Some A are B
Some B are A(2)’

Some A are A
M ost A are A(5)’

Some A are B
Some A are A

一般化量化子を含む自然論理に対する依存型意味論の完全性

L(all, some, no, names)、L(most, some) に対する依存型意味論の完全性を示したい。依存型意味論 [1] の枠組みで Moss [2] の Syntax を表すとそれぞれ以下のようになる*2 。ここでは “most” の表現は 2 章で紹介した Tanaka & Nakano & Bekki [3] の most の定義に基づく。また Moss [2] は依存型意味論の特徴の一つである動的な分析が可能ではない。従って推論規則の前提と帰結では共通の文脈が与えられているとする。
Moss [2]依存型意味論All A are B(Πu : (Σx : E)Axδc)B(π1 (u))(δ ∧ (Σx : E)Axδc)(c, u)Some A are B(Σu : (Σx : E)Axδc)B(π1 (u))(δ ∧ (Σx : E)Axδc)(c, u)

N o A are B(Πv : (Σu : (Σx : E)Axδc)B(π1 (u))(δ ∧ (Σx : E)Axδc)(c, u))⊥J is an A(Σv : (Σx : E)Axδc)eq(E, π1 (v), j)

J is Seq(E, j, s)

M ost A are B(Σk : N)(k ≥ [ 1π (sel|(Σx:E)Axδc|≥1 (c))+1]+12∧(Σf : M (k) → (Σx : E)Axδc)(f is an A-injection∧(Πy : M (k))(B(π1 (f y))(δ ∧ (Σx : E)Axδc)(c, f y))))例として L(most, some) の推論規則 (1)’ が完全であることの証明は次のようになる。
推論規則 (1)’ の完全性
Aczel 1980 によって提案された Mr シーケンスを使って有限集合を構成する。その定義は以下である。*3M (n)
f (n)

def

≡

R(n, ⊥, (λx)(λy)f (x)) : type (n : N)def

R(n, ⊤, (λx)(λy)(y + ⊤)) : type (n : N)≡

証明の詳細は省略するが、(ΣE) 規則、(NE) 規則を適用することで前提 m : M ost A are B から型 M (π1 (m))の proof term a を構成でき、推論規則 (1)’ は証明 1 のように示すことができる。
L(all, some, no, names)、L(most, some) のそれぞれの推論規則に対して上記のような証明を施すことによって、依存型意味論においてこれらの推論規則が表現可能であるを示すことができる。なお現段階で、推論規則 (2)’(3)’ の完全性については示せていない。この二つの推論規則の完全性を示すことは今後の課題である。
とくに推論規則 (3)’ について構成的型理論の枠組みで示すならば、背理法を用いずに示さなければならない。
なぜなら構成的型理論では排中律 (A ∨ ¬A) 及び、二重否定除去 (¬¬A → A) の規則は成立しない。背理法に*1 Moss [2] では L(most, all, some) の推論規則の完全性はまだ示せていない。
*2 E は Entity を表す*3 f (n) の + は coproduct 演算子

よる証明が妥当であることと排中律は同値であり、この推論規則の完全性について背理法を用いて示すことは、構成的型理論の範疇を超えてしまう。この推論規則の完全性を構成的型理論の枠組みで示すならば、背理法や排中律、二重否定除去の規則を用いずに示す必要がある。もしこれらの規則を用いずに推論規則 (3)’ の完全性が示せないならば、Moss [2] システムは構成的型理論では表現できない可能性があることになる。
この二つの推論規則の完全性を示すことができるな
らば、依存型意味論は L(most, some) の推論規則に対して完全であることを示すことができる。
一方 Moss [2] では L(all, some, most) の推論規則を持たないので、以下の妥当な推論はできない。
All A are B M ost C are A
M ost C are B

この推論が依存型意味論において可能な推論であることを示すことは今後の課題である。この推論が依存型意味論において可能であるならば、Moss [2] のシステ
ムでは動的な分析が可能ではないこと、依存型意味論で可能である、先行詞に対する照応も表現することができないことと合わせて、依存型意味論が Moss [2] のシス
テムより強いことを示すことができる。

5

まとめ

本研究では、L(all, some, no, names) に対する依存型意味論の完全性を示し、また L(most, some) の推論規則 (1)’(4)’(5)’ に対する依存型意味論の完全性を示した。
今 後 の 課 題 と し て 、L(most, some) の 推 論 規 則(2)’(3)’ の完全性を示すこと、「All A are B, M ost C are A ⊢ M ost C are B 」のような L(all, some, most) の推論規則が依存型意味論において可能な推論であることを示すことなどがある。

参考文献[1] Bekki, Daisuke. (to appear). Dependent Type Semantics: An Introduction, the 2012 edition of theLIRa yearbook: a selection of papers, Universityof Amsterdam, 2012.
[2] Moos, L.S. Completeness Theorems for Syllogistic Fragments., In:Hamm, F, Kepser, S.(eds.)
Logics fpr Linguistic Structures, Mouton deGruyter, Berlin, pp.143-173, 2008.
[3] Tanaka, R. and Nakano, Y, and Bekki, D. Constructive Generalized Quantifiers Revisited, In:
Proceedings of the Tenth International Workshop
on Logic and Engineering of Natural Language
Semantics (LENLS10), the ﬁfth JSAI International Symposia on AI 2013, Tokyo, Japan, pp.6978, 2013.