日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

漸進的論理のシークエント計算
蟻坂竜大

漸進的論理は私が以前考案した論理体系の日本語直訳であり、属性を持つ概念の推論を念頭におく。特有の論理記号として ⋗ を持ち、P1 ⋗ P2 はおおよそ、“P1 は P1 を論じる領域内の真により真であり、真である場合には P1 はP2 を論じる領域を属性として持ち、その領域内の P1 の真に依存する真により P2 は真である。” という命題である。体系というわけだから種類はひとつではないが、この論文内では一番初めに構想した漸進的論理の解釈に基づきシークエント計算を示す。

明確な差別を仮定しない。例えば前述の本と表題と1 はじめにいう２つの概念があるとしよう。本は主概念であり、漸進的論理とは私が以前考案した論理体系である

表題はその属性であるとしても、表題を持つ本はまた[2] [3]。命題論理の論理記号に ⋗ を加え、P1 ⋗ P2 を主概念となり、それ自体属性を持つだろう。さらに表

おおよそ、P1 は P1 を論じる領域内の真により真で題を持つ本自体また何かしらの主概念の属性となりあり、真である場合には P1 は P2 を論じる領域を属うる。そういった概念の相互作用に関する理解が重要性として持ち、その領域内の (P1 の真に依存する) 真であろうことは RDF などの知識を必要とするまでもにより P2 は真である、という命題とする。引用元のないだろう。であるから、流行かどうかはさておき、ように存在を主に扱う場合には、例えば 本 ⋗ 表題 が私は漸進的論理は自然言語の特徴を捉える上で重要あるとすると、これは本という概念が、論じられてな論理であると信じて疑わない。

いる領域内にあり、その概念は表題という概念を属性論理の原理は [2] [3] で既に記したのでそちらを参照に持つ、となる。ちなみに、考案から実に２年が経っしていただければよいが、ここでは [2] で用いられたたが、その存在意義は現在のところ私自身のみにしSemantics を振り返る。定理等は証明されたものとか知られていない。しかし、漸進的論理が取り扱う題し、一切触れない。シークエント計算は Semantics

材を考察してみるに、この論理は McCarthy によるを定義後に示す。専門用語があやふやなので所々英語

Context Logic [6] よりも一般的に Context を扱うこになってしまうところはご容赦いただきたい。漸進とができ、Context が何かという根本の問題も棚上げ的論理の証明論が示されるのは今回が初めてとなる。

しない。Relevant Logic [1] のように矛盾許容の領域に飛び込まずとも関連性を表現できる。†1 またこの

なお、本来ならば漸進的論理の原理や実用性をより論理は最小表現の存在や Term-Predicate 間の従来のめ、この論文内では省かせていただく。

A Sequent Calculus for Gradual Logic
Ryuta Arisaka, , .
†1 (本 ⋗ 表題) ⊃ 本:“表題を持つ本は本である。” 一般的に P1 ⋗(P2 ⋗(P3 ⋗(· · ·⋗Pk ))) は矛盾していなければ必然的に P1 であり、P1 ⋗ P2 であり、P1 ⋗ (P2 ⋗ P3 )であり、P1 ⋗ (P2 ⋗ (· · · ⋗ Pk−1 )) である。

深く論じるべきなのだが、 [3] が現時点で査読中のた2 関連研究関連研究を挙げるほどの研究がなされていないが、漸進的論理に概念上関連すると思われるものとして、フラクタルを挙げておく。漸進的論理はプログラム理論、認識信念論理、信念改訂理論 [4] [5]、オントロジー理論などへ応用できる。

3 背景:Semantics
Literal の集合は A で表す。構成員は a を使って指す。命題論理の規則に従い、a ∈ A ならば ac ∈ Aが成り立つ。ここで ac は a の complement であり、(ac )c = a である。A に ⊤ と ⊥ を加えたものを S で表す。その構成員は s で指す。そうすると、漸進的論理の論理式 (F を使う) は以下の文法が認識するものとなる。F := a | ⊤ | ⊥ | ¬F | F ∧F | F ∨F | F ⋗F .とする。∧† と ∨† はブール代数の operators とする。
†2
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.

[M |= s0 ⋗ s1 ⋗ · · · sk ] = J (s0 .s1 . . . . .sk ).
[M |= F1 ∧ F2 ] = [M |= F1 ] ∧† [M |= F2 ].
[M |= F1 ∨ F2 ] = [M |= F1 ] ∨† [M |= F2 ].
各 s ∈ S につき、¬s 7→ sc .
¬(F1 ∧ F2 ) 7→ ¬F1 ∨ ¬F2 .
¬(F1 ∨ F2 ) 7→ ¬F1 ∧ ¬F2 .
¬(s ⋗ F ) 7→ sc ∨ (s ⋗ ¬F ).
(F1 ⋗ F2 ) ⋗ F3 7→(F1 ⋗ F3 ) ∧ ((F1 ⋗ F2 ) ∨ (F1 ⋗ F2 ⋗ F3 )).
F1 ∧ F2 ⋗ F3 7→ (F1 ⋗ F3 ) ∧ (F2 ⋗ F3 ).
F1 ∨ F2 ⋗ F3 7→ (F1 ⋗ F3 ) ∨ (F2 ⋗ F3 ).
F1 ⋗ F2 ∧ F3 7→ (F1 ⋗ F2 ) ∧ (F1 ⋗ F3 ).
F1 ⋗ F2 ∨ F3 7→ (F1 ⋗ F2 ) ∨ (F1 ⋗ F3 ).

使用されている論理記号のうち ∧ と ∨ は associativeあ る F の 与 え ら れ た domain function 下 で のまた commutative であるが、⋗ は right-associative(un)satisfiability また (in)validity の定義は次のよである、commutative ではない。結合優先順位であうになる。F が satisfiable ならば [M |= F ] = 1 とるが、基本的に命題論理の通り、⋗ は優先順位最下なる valuation frame M がある。その逆も成り立位とする。さて、Semantics の定義へ向かう。S ∗ につ。F が valid ならば全ての valuation frame M でより、S の有限列の集合に {ϵ}、長さが 0 の列、を

[M |= F ] = 1 となる。その逆もなりたつ。F が in-足したものを表すことにする。そして以下のようにvalid ならば [M |= F ] = 0 となる valuation frame∗

Sdomain function D : S → 2 と valuation frame

M がある。その逆も成り立つ。F が unsatisfiable な(I, J ) (I : S × S → {0, 1},J : S \{ϵ} → {0, 1})

らば全ての valuation frame M で [M |= F ] = 0 となを定める。

る。その逆も成り立つ。与えられた domain function• 各 s∗ ∈ S ∗ で、D(s∗ ) は complementation の下でにおいて [M |= F ] が 0 とも 1 ともならない F はそ∗∗閉じており、少なくとも ⊤ と ⊥ を含む。
∗∗∗∗

• 各 s ∈ S で I(s , ⊤) = 1、また I(s , ⊥) = 0.
∗ない。

∗• 各 a ∈ D(s ) で、I(s , a) は 0 か 1 であるが、両方ではない。また、I(s∗ , a) が 0 ならば I(s∗ , ac )4 シークエント計算

は 1 であり、I(s∗ , a) が 1 ならば I(s∗ , ac ) は 0 で

この論文の目的であるシークエント計算の定義であるがまず構造を次の文法で定める。

ある。

•の domain function 下で無効な論理式とし、考慮し各 s∗1 , s∗2 ∈ S ∗ 、また各 a ∈ D(s∗1 ) ∩ D(s∗2 ) で、s∗1Γ := F | • Γ | Γ; Γ | Γ ←- Γ.と s∗2 の長さが同じならば I(s∗1 , a) = I(s∗2 , a) が成

ここで構造記号である ←- は right-associative、同じり立つ。

く構造記号である ; は commutative また associative• 各 s0 .s1 ....sk ∈ S ∗ \{ϵ} で、J (s∗ ) = 1 ならば各 0である。結合順は、•、; 、←- の順だが、• の優先順

以上 k 以下の長さ i において、I(s0 ...si−1 , si ) = 1

位はいずれの論理記号のそれよりも劣る。 シークエであり、反対も成り立つ。なお、i = 0 のとき、ント計算の規則上で現れる構造は実際にその規則がs0 ....si−1 = ϵ とみなす。

instantiate された時に空になる場合があるので、こ∗∗• 各 s0 .s1 ....sk ∈ S \{ϵ} で、J (s ) = 0 ならばある
0 以上 k 以下の長さ i において、I(s0 ...si−1 , si ) = 0であり、反対も成り立つ。
これらの定義を用いて下のように forcing relation |=、また変換規則を定める。なお、M は valuation frame†2 変換規則を定義せずとも Semantics の定義は可能で、その場合には J に全く触れずに定義できるが、結局煩雑になるのであまり推奨されない。また、この定義リ
スト中、８番目、9 番目、１０番目に見つかる変換規則がない場合 ( [3] を参照されたい) の方が Semanticsは複雑になる。ここでは触れない。

れ以降、構造を記す必要がある場合には、空であるか合には、そのシークエントを id もしくは ⊤ によりもしれない構造の上部には tilde を入れ、明確にする。

即座に閉じてよい。何故かといえば、両シークエン

f1 ; Γ2 とあり、Γ1 が空の時は、この構造は単に仮に Γト共に正の Context をもち、正の Context 内では ;f1 ←- Γ2 とあり、Γ1 が空の時は、Γ2 である。仮に Γは ∨ と捉えて差し支えないからである。その一方この構造は単に Γ2 である。他の場合も同様に考える。

で、例えば ⊢1 ⋄ (a ←- Γ1 ); (ac ←- Γ2 ) が現れても、さて、空であるかもしれない構造が与えられたとき iそのシークエントを即座に閉じることはできない。

f1 ⋄ Γ
f2 をシークを 1 か 2 のどちらか一方として、⊢i Γ

Semantics によれば、I(ϵ, a) = 1 の場合には ⊢1 Γ1エントと呼ぶ。i = 1 の時、特に第一種シークエントとの closed derivation tree を構築できることを、ま呼ぶ。同様に i = 2 の時、特に第二種シークエントとた I(ϵ, ac ) = 1 の場合には ⊢1 Γ2 の closed deriva-呼ぶ。最後に Context を次の文法で定める。Ω(−) :=tion tree を構築できることを示さねばならない。

− | Ω(−) ←- Γ | Γ ←- Ω(−) | Γ; Ω(−) | Ω(−); Γ | • Ω(−).

⊢1 ⋄ (a1 ←- Γ2 ); (ac1 ←- Γ3 ); (a2 ←- Γ4 ); (ac2 ←- Γ5 )ここで − には構造が代入されるものとし、構造が代入など、構造が多い場合には worst case ではよりたくされた Context は構造である。与えられた Context、さんの場合を考える必要がある。そういった場合の生Ω(−)、が 0 を含む偶数個の同一でない •Ω′ (−) を成は第２種推論で行なわれ、⋄ の左側が使用される。

sub-context として持つ場合、特にその Context をそして、その左側は ↓ を経由して ⋄ の右側へ送られ、+正の Context と呼び、Ω(−) と明確にする場合もあ−再び第一種推論が行なわれる。前セクションで与えたる。奇数の場合は特に負の Context と呼び、Ω(−)

Semantics 下での漸進的論理の論理式の validity の推と明確にする場合もある。例として、仮に Ω(−) が論はこの繰り返しで行なわれる。

• • − ならば Ω1 (−) と Ω2 (−) をそれぞれ •− と − とすれば、Ω(−) は •Ω1 (−) と •Ω2 (−) の２つの sub-5 まとめと今後の課題

context をもつことになるので、この場合 Ω(−) は正

ここでは漸進的論理のシークエント計算を示した。の Context となる。これで必要な定義は揃った。漸厳密な Soundness、Completeness の証明を Coq を進的論理のシークエント計算を図 1 に記す。全ての用いて行なってゆく。

場合についての証明は行なっていないものの、考慮に値する †3 論理式 F が valid ならば、⊢ F を帰結と1する closed derivation tree を図 1 の規則を使用して構築できる、と見られる。また、⊢1 F を帰結とする

closed derivation tree を図 1 の規則を使用して構築できるならば、F は valid である、と見られる。
以下、図 1 の規則への若干の説明を行ない、現セクションを締めくくる。まずお気づきいただきたいが、第一種シークエントの推論では、⋄ の左側は全く関係してこない。そして、第一種推論の役割は前セクションで挙げた変換規則の実現、また、命題論理の推論を行なうことに限定される。その推論の過

e a; ac もしくは ⊢1 ⋄ Γ;e ⊤ が現れる場
程で ⊢1 ⋄ Γ;

†3 前述。

参 考 文 献[1] Anderson, A. R. and Belnap, N. D.: Entailment: The Logic of Relevance and Necessity, Vol. 1,Princeton University Press, 1975.
[2] Arisaka, R.: Gradual Classical Logic for Attributed Objects, ArXiv e-prints:1404.6036, (2014).
[3] Arisaka, R.: Gradual Classical Logic for Attributed Objects - Extended in Re-Presentation,
ArXiv e-prints:1504.04802, (2015).
[4] Arisaka, R.: How do you revise your belief set
with %$￡;@*?, ArXiv e-prints:1504.05381, (2015).
[5] Arisaka, R.: Latent Belief Theory and Belief Dependencies: A Solution to the Recovery Problem inthe Belief Set Theories, ArXiv e-prints:1507.01425,(2015).
[6] McCarthy, J.: Notes on Formalizing Context, IJCAI, Morgan Kaufmann, 1993, pp. 555–562.

f1 ; Γ2 ⋄ Γf3⊢2 Γeval1ff3⊢2 Γ1 ⋄ (⊤ ←- Γ2 ); Γf1 ; Γ2 ⋄ Γf4f1 ; Γ3 ⋄ Γf4⊢2 Γ⊢2 Γeval2cff⊢2 Γ1 ⋄ (a ←- Γ2 ); (a ←- Γ3 ); Γ4⊢2 ⋄ Γ2↑⊢1 ⋄ Γ2f2⊢2 Γ1 ⋄ Γ

ide a; ac⊢1 ⋄ Γ;⊢1 ⋄ Ω(F1 )+e ⊤⊢1 ⋄ Γ;⊢1 ⋄ Ω(F2 )+⊢1 ⋄ Ω(F1 ∧ F2 )⊢1 ⋄ Ω(F1 )−⊢1 ⋄ Γ1+⊢1 ⋄ Ω(F2 )−−⊢1 ⋄ Ω(F1 ∨ F2 )⊢1 ⋄ Ω(sc ; (s ←- •Γ))+⊢1 ⋄ Ω(•(s ←- Γ))∧+∨−⊢1 ⋄ Ω(•F )¬⊢1 ⋄ Ω(¬F )⊢1 ⋄ Ω(F1 ; F2 )−⊢1 ⋄ Ω(sc )red1⊢1 ⋄ Ω(•s)−⊢1 ⋄ Ω(F1 ∧ F2 )∧−⊢1 ⋄ Ω(Γ1 ; Γ2 ←- Γ3 )+⊢1 ⋄ Ω(Γ1 ←- Γ2 ; Γ3 )+⊢1 ⋄ Ω((Γ1 ←- Γ2 ); (Γ1 ←- Γ2 ←- Γ3 ))+⊢1 ⋄ Ω(s ←- •Γ)−

⊢1 ⋄ Ω(•(s ←- Γ))

−

red−
2

⊢1 ⋄ Ω(Γ1 ←- Γ2 )−⊢1 ⋄ Ω(Γ1 ←- Γ3 )−red+
5⊢1 ⋄ Ω(Γ2 ←- Γ3 )−⊢1 ⋄ Ω(Γ1 ; Γ2 ←- Γ3 )−⊢1 ⋄ Ω(Γ1 ←- Γ3 )−⊢1 ⋄ Ω(Γ1 ←- Γ2 ; Γ3 )−⊢1 ⋄ Ω((Γ1 ←- Γ3 ); (Γ1 ←- Γ2 ))−red−
4⊢1 ⋄ Ω((Γ1 ←- Γ3 ); (Γ1 ←- Γ2 ←- Γ3 ))−⊢1 ⋄ Ω((Γ1 ←- Γ2 ) ←- Γ3 )−⊢1 ⋄ Ω(Γ1 )Wk⊢1 ⋄ Ω(Γ1 ; Γ2 )
図1

red+
3red+
4

⊢1 ⋄ Ω((Γ1 ←- Γ2 ) ←- Γ3 )+⊢1 ⋄ Ω(sc )−∨+⊢1 ⋄ Ω(F1 ∨ F2 )+⊢1 ⋄ Ω(F1 ←- F2 )⋗⊢1 ⋄ Ω(F1 ⋗ F2 )⊢1 ⋄ Ω((Γ1 ←- Γ2 ); (Γ1 ←- Γ3 ))+⊢1 ⋄ Ω(Γ1 ←- Γ3 )+⊢1 ⋄ Ω(F1 ; F2 )+⊤⊢1 ⋄ Ω((Γ1 ←- Γ3 ); (Γ2 ←- Γ3 ))+red+2+↓⊢1 ⋄ Ω(•Γ1 ; •Γ2 )dist⊢1 ⋄ Ω(•(Γ1 ; Γ2 ))GradC: 漸進的論理のシークエント計算

red−
5

red−
3