前提のための動的論理の証明論構築に向けて石下裕里

1(指導教員：戸次大介)

はじめに

「前提」
CCG の意味表示として高階動的論理を用い、の意味論も扱っている。また、複数オブジェクトや量化を扱えるように拡張されている。動的命題は型付きラムダ計算を用いて定義されているため、PUL よりも証明論的であるが、動的論理の証明も型付きラムダ計算を媒介するため、間接的である。

形式意味論の手法に基づいて文の意味構造を明らかにするうえで、実世界のデータ（母語話者の直観による文間の含意関係の有無）と、文と文の関係を決定づける理論装置（命題間の含意関係を定義している論理システム）は必要不可欠である。意味の構造が明らかになり形式的な記述が可能になることで、自然言語処理における意味解析の発展につながることが期待されている。ところが、自然言語の現象の一つである「前提」の形式化については昔からその是非が問題とされてき「前提」の分析にはた。現在では、Heim (1983) 以来、動的論理を用いたモデル理論的意味論が主流となっている。それに対して、戸次 (2010) では証明論的意味論が与えられているが、その証明システムは動的論理に対しては間接的である。そこで本研究では、動的命題を様相演算子とみなす Fischer and Ladner (1979) の考え方に立ち返り、動的論理に対する直接的な証明システムを与えることを試みる。

2

高階動的論理 [戸次 (2010)]

3.3

4

証明論の構築3 章で説明した動的論理の特徴を踏まえ、本研究では、PDL の意味論として戸次 (2010) を改良し、「前提」を直接記述できるような証明システムの構築を試みる。
統語論

4.1

戸次 (2010) で用いられている演算子のほか、本研究では新たに PDL の演算子（?,  , [ ], |）を導入する。
p, q, r, . . . ： 動的命題

φ, ψ, . . . ： 命題の集合「前提」; , |, ε, ∼, Δ, ∂ ： 動的命題演算子¬, ∧, ∨, →, ⊥,： 命題演算子「前提」とは、言語的表現が意味を持つために満たさなければならない特別な状態のことである。例えば、
以下の例文において、文 2 の命題は文 1 の命題の「前提」となっている。
1. The king of France is bald.
2. There is a unique king of France.
命題 A が、文 S が表す命題 B の「前提」となり得るのは、A が B に含意されるだけでなく、文 S を否定文・条件文の前件部・蓋然文に埋め込んだ際にも埋め込んだ文が表す命題に A が含意される場合に限られる。この性質により、「前提」は静的な論理である古典論理では記述できないことが知られている [Beaver (2001)]。

各命題の直感的な意味は、次のとおりである。

3

4.2?,  , [ ] ： 混合演算子
p; q, p | q, φ?, εx, ∼p, Δx(p), ∂(p) ： 動的命題
¬p, φ ∧ ψ, φ ∨ ψ, φ → ψ, pφ, [p]φ ： 静的命題
pφ ： p を実行後、φをみたす状態が存在する.
[p]φ ： p の実行後はいつでも、φをみたす状態へ移る.
p; q ： p を実行し、その後 q を実行する.
p | q ： p と q のどちらか一方を選択し、実行する.
φ? ： φが真ならば続行、偽ならば停止する.

動的論理

各演算子の意味は次のようなものである。
定義（動的論理式）

動的論理は、プログラミング理論から派生した論理であり、従来の論理と異なるのは、命題を「文脈と文脈との関係」として扱う点である（このような命題を「動的命題」と呼ぶ）[Pratt (1976)]。本研究では、以下の 3 つの文献で使用されている動的論理に着目した。

3.1

意味論

def≡

λG.λH.(H = (G∩λg.(g ∈ G ∧ π1 (g), . . . , πn (g) ∈ R)))

def≡

λG.λH.∃K.(pGK ∧ qKH)

def

≡λG.λH.(pGH ∨ qGH)

def

≡λG.λH.(H = G) ∧ φG

def≡

λG.λH.(H = G × (λx. ))(ただし、G ∈ P ow(en ))

∼p

def

≡

([p]⊥)?

Δx(p)

def

≡

λG.λH.(H = λg.∃d.∃K.(g ∈ K)∧p(σx=d (G))K)def

λG.λH.(pGH ∧ (G = πx1 ,...,xn (H)))

R(x1 , . . . , xn )p; qp|q

PDL[Fischer and Ladner (1979)]φ?

PDL(Propositional Dynamic Logic) は、動的命題を様相演算子とみなす手法により動的論理を一種の様相論理として扱い、直接的な証明論を与えている。しかし、プログラミング言語の意味論として構築されたものであり、自然言語の意味論との対応は考慮されていない。

εxn+1∂(p)
skip

3.2

PUL[Beaver (2001)]≡def

λG.λH.

≡λG.λH.⊥σx=a (G)def≡

λg.(g ∈ G ∧ g(x) = a)

πi,j,... (G)defλg.∃h.(h ∈ G ∧ h = πi (h), πj (h), . . .)failPUL(Partial Update Logic) は、動的論理を用いた「前提」の記述を試みている。しかし、PUL はモデル理論的意味論によって定義されているため、実際に「前提」を証明論的に計算していくには不向きである。

≡def

ただし、

13≡定義（静的論理式）

[p]φdef≡λG.∀H.(pGH → φH)

pφ

def

≡λG.∃H.(pGH ∧ φH)

φ∧ψ

def

≡λG.(φG ∧ ψG)

φ∨ψ

def

≡λG.(φG ∨ ψG)

φ→ψ

defλG.(φG → ψG)

¬φdef

≡
≡λG.(¬φG)

def≡≡λG.⊥def

φ1 , . . . , φn  ψ ≡ φ1 ∩ · · · ∩ φn ⊆ ψPDL の公理とその健全性

4.3:

Mnotonicity of [p]:Hoare composition rule:Γ φ→ψp φ → p ψ
Γ φ→ψΓ [p]φ → [p]ψ
Γ {φ}p{ρ},Γ {ρ}q{ψ}Γ {φ}p; q{ψ}
Γ「前提」の記述

 ここで、4 章で構築した体系を用いて「前提」を含 む文の意味構造を以下のように記述することが可能となる。
1. The king of France is bald.
∂(εx; koF (x)); bald(x)
2. The king of France is not bald.
∼(∂(εx; koF (x)); bald(x))


定義（意味論的推論）
Monotonicity of p5

λG.

def⊥

また、このほかにも、以下が許容規則であることが証明できる。

以下は、Harel et al. (2000) における PDL の部分体系である。

6


PDL の公理

本研究では、戸次 (2010) を拡張する形で新たに動的論理式・静的論理式を型付きラムダ計算によって定義し、その体系に対して PDL に基づく証明システムが健全であることを示した。また、そこから導かれる定理と許容規則を証明し、2 章の例文について「前提」がどのように記述できるかを提示した。
 今後の課題としては、ε, ∼, Δ, ∂ 等に対応する PDL
 の公理を発見し、戸次 (2010) の動的論理に対してより完全な証明システムを構築することが挙げられる。

PDL の公理は、命題論理の公理に以下を与えたものである。
[p](φ → ψ) → ([p]φ → [p]ψ)[p](φ ∧ ψ) ↔ [p]φ ∧ [p]ψ[p | q]φ ↔ [p]φ ∧ [q]φ[p; q]φ ↔ [p][q]φ[φ?]ψ ↔ φ → ψp φ ↔ ¬[p]¬φ
PDL の推論規則
Modus ponens(MP):Modal generalization(MG):φ, Γ φ → ψΓ ψΓ φ
Γ [p]φΓ

参考文献

4.2 節の意味論に対する健全性を証明する。
定理（PDL の健全性）


証明．公理 [p](φ → ψ) → ([p]φ → [p]ψ) の場合：Harel, D., D. Kozen, and J. Tiuryn. (2000) DynamicLogic. MIT Press.

[p](φ → ψ) → ([p]φ → [p]ψ)≡ λG.∀H.(pGH → (φ → ψ)H) → (λG.∀H.(pGH → φH) → λG.∀H.(pGH → ψH))
≡ λG.∀H.(pGH → (φH → ψH)) → (λG.∀H.(pGH → φH) → λG.∀H.(pGH → ψH))
≡ λG.(∀H.(pGH → (φH → ψH)) → (∀H.(pGH → φH) → ∀H.(pGH → ψH)))

(→E)
(→E)

pGA(3)(∀E)∀H.(pGH → φH)
pGA → φApGA(3)(∀E)∀H.(pGH → (φH → ψH))

Heim, I. (1983) “On the Projection Problem forPresuppositions”, In the Proceedings of the West
Coast Conference of Formal Linguistics II.pp.114126.

(1)

pGA → (φA → ψA)φA → ψA

ψA(→I)

(→I)

(→E)

φA

pGA → ψA

(∀I)
(→I)

(2)

∀H.(pGH → ψH)∀H.(pGH → φH) → ∀H.(pGH → ψH)∀H.(pGH → (φH → ψH)) → (∀H.(pGH → φH) → ∀H.(pGH → ψH))

(3)

(2)
(1)

Pratt, V. (1976) “Semantical Considerations on
Floyd-Hoare Logic”, In the Proceedings of 17th
Annual IEEE Symposium on Foundations of Computer Science. pp.109–121.

他の公理を含めた証明の詳細は、石下・戸次 (2011)を参照されたい。

4.4

Beaver, D. I. (2001) Presupposition and Assertion in
Dynamic Semantics, Studies in Logic, Languageand Information. CSLI Publications & folli.

Fischer, M. and R. Ladner. (1979) “Propositional Dynamic Logic of regular programs”, Journal of Com
puter and System Science 18(2), pp.194–211.

PDL φ ⇒ Γ  φΓ

まとめと今後の課題

PDL の定理

前節の証明システムを用いて、以下の定理を導くこ戸次 大介, 2010. 「日本語文法の形式理論−活用体系・とができる。
統語構造・意味合成−」, 日本語研究叢書 24, くろ.
しお出版
PDL の定理
p φ ∧ [p]ψp (φ ∨ ψ)p | q φ
p; q φψ? φ
p (φ ∧ ψ)[p]φ ∨ [p]ψ

→↔
↔
↔
↔
→→

p (φ ∧ ψ)p φ ∨ p ψp φ ∨ p ψp q φ
ψ∧φ
p φ ∧ p ψ[p](φ ∨ ψ)

石下 裕里, 戸次 大介, 2011. 「命題動的論理の証明システムとその健全性について」, Tecnical Report ofDepartment of Information Sciences, Ochanomizu
University, OCHA-IS 10-3, February 7th, 2011.

14