JAIST Repository
https://dspace.jaist.ac.jp/
Title
Residuated latticeおよびContractionルールを持たない論理の分類に関する研究
Author(s)
上田, 正樹Citation
Issue Date
2000‑03Type
Thesis or DissertationText version
authorURL
http://hdl.handle.net/10119/1338Rights
Description
Supervisor:小野 寛晰, 情報科学研究科, 修士logics without contraction rule
上田 正樹
北陸先端科学技術大学院大学 情報科学研究科
2000
年
2月
15日
キーワード: 部分構造論理,contractionrule,residuated lattice,論理の強さ,variety.
1
序論
人間が日常的に思考を行う際に使用する一般的な法則を見い出すために、従来、古典 論理、直観主義論理に代表される様々な論理が研究されてきた。そして、90年代以降は、
我々の推論の実際に基づいた論理を構築するため、ならびに論理規則の意味およびその性 質を研究するために、contractionルールやweakeningルールといった、古典論理、直観 主義論理の有する構造規則の一部を有さない論理、すなわち部分構造論理の研究が盛んに 行われてきている。本論文では、これらの構造規則のうち、contractionルールに着目し
た。Contractionルールを持たない論理は、資源の論理とも呼ばれ、ある命題が 幾つ存在
するかを考慮することが容易な論理であり、人間の思考形態との一致性から見ても重要な ものであるからである。
P;P !Q
P P !Q
Contractionルールのない論理は上記のような推論規則を有する。は融合積と呼ばれ
る演算を行うものであり、P P は、この論理式においてP という命題が二つ存在してい ることを意味している。
Contractionルールを持たない論理を取り扱うに際し、本論文では、residuated lattice という代数構造を用いた意味論からのアプローチを行った。１）小野により導入された
contractionルールを持たない論理の分類体系fWngnの研究[3]を紹介し、その分類体系 が公理化という視点から見てどのようなものであるのか、および各クラスWnにおける論 理の強さはどのようになっているのか、についての結果を得た。２）Contractionルール
Copyrightc 2000byMasakiUeda
を持たない論理のうち、二重否定規則が成立する論理に対し、有限モデル性を有するもの と有さないもの、および有限公理化可能かつ有限モデル性を有さないものがどれだけ存在 するかについての結果を得た。
2 Contraction
ルールを持たない論理
Contractionルールを持たない論理を考える際に、その基本となる論理として古典論理
ClとFLew を考える。FLewとは、直観主義論理Intからcontractionルールを取り除い た論理であり、BCK 論理ともいわれる。
FL
ewでは、二重否定規則::pp、排中律:p_p、分配則といった古典論理Clで成 立する諸公理が成立しない。ここで論理というものを、恒真になる論理式の集合として捉 えると、FLewは、構造規則としてcontractionルールのみを持たない論理のうち、最も 小さい集合として捉えることができる。逆に、古典論理Clは、最も大きい集合となって いることになる。以後、contraction ルールを持たない論理を考える際、このFLewから
Clまでの間の論理を扱うことにする。また、論理の強さという概念を導入し、論理Aで 恒真となる論理式の集合が、論理Bで恒真となる論理式の集合を包含するとき、論理A は論理Bより「強い」論理である、と定義する。
3 Residuated lattice
とその分類体系
fWngn古典論理Clは、その意味論としてブール代数という代数構造をとることができる。す なわち、真=1；偽=0として、論理演算子を代数演算に置き換えて対応関係を維持させ ることにより、論理式を代数構造上で扱うことが可能である。Contractionルールを持た ない論理の意味論についても、同様の代数構造を考えることができる。このとき、その代 数構造はresiduated latticeとなる。代数M=hM;\;[;;!;0;1iがresiduated latticeに なるとは、Mが以下の条件を満たすことである。
1. hM;\;[;0;1iが、最小元 0、最大元 1 を有する束である
2. hM;;1iが交換法則を満たすモノイドである
3. x;y2M に対し、xyz, xy !z.
Residuated latticeにおけるが、論理式演算における融合積に対応している。
このresiduatedlatticeで表わされる論理を、小野は以下の等式Ekに基づいて分類した。
E
k :x
k
=x k+1
すべてのMについて、Mの任意の要素に上記等式Ekが成立する。ここで、ある論理M が分類Wnに属するとは、Mの全ての要素についてEnが成立し、ある要素については
E
n 1が成立しないことをいう。この分類体系fWngnについて幾つかの新しい結果を得た。
4
分類
Wnに関する結果
小野は[3]において、EM,DN,Con,WCon,P,WP,Lin,Disなどの公理を導入し、その相互 関係を示している。一方、古典論理の次に強い論理についての考察を行い、特に有限の
residuated latticeが古典論理の次に強い論理となるための条件を与えている。
nが素数の場合には、Lukasiewiczのn+1値論理はWnに属し、しかも古典論理の次に強い 論理になることは容易に判る。[3]では、simpleでもlinearでもないようなresiduatedlattice でそのような論理を定めるものの例が与えられている。SimpleかつlinearでLukasiewicz
の多値論理のモデルとは異なるものでそのような性質を持つものが存在するか否かは未 解決のまま残されている。
この論文では、Wnの構造について以下のような結果を得た。
1. 古典論理の公理DN,WCon,Lin,Disのうち、いくつかをFLew に付加した論理であっ て、かつDNとWConを同時には満たさないものが、W!に存在している。
2. n3に対し、各Wnは、Lukasiewiczの多値論理とは異なる、simpleかつ線形な古 典論理の次に強い論理を有する。これにより、上記の問題が解決された。
3. n2に対し、各Wnは、古典論理の次に強い論理を少なくとも可算個有している。
5 Variety
の導入
最後に、[4]をもとに、FLew に二重否定規則を公理として付加した論理：FLew[DN]を 決定するlatticeであるclassical residuated latticeに対してvariety（等式で表わされる論 理の集合）を導入し、contractionルールのない論理における有限モデル性と有限公理化 に関しての検討を行い、以下の結果を得た。
1. FL
ew
[DN]の拡張体系となる論理のうち、有限モデル性を持つもの、およびそれを 持たないものは、それぞれ非可算個存在する。
2. FL
ew
[DN]の拡張体系となる論理のうち、有限モデル性を持たないものであって、か つ有限公理化可能なものが可算個存在する。
6
結論および今後の課題
本論文で得られた主要な結果は以下の通りである。
n2ならば、恒にWnには古典論理の次に強い論理が少なくとも可算個存在する。
FL
ew
[DN]の拡張体系となる論理のうち、有限モデル性を持つもの、およびそれを 持たないものは、それぞれ非可算個存在し、有限モデル性を持たないもののうち、
有限公理化可能なものが可算個存在する。
今後の課題としては、W!には幾つのClの次に強い論理が存在するか、各Wnにおい て、DN,WCon,Lin,Disといった公理を真にする論理でかつClの次に強い論理が幾つ存在 するか、Wnと直交するような形のvarietyが存在するのか、存在するのであればそれを分 類体系として採り入れられないか、等の研究が期待される。より詳細にcontractionルー ルを持たない論理の分類が確定し、その分類に属する論理の特徴が把握できるようになる ことを期待したい。
参考文献
[1] Blok,W. and Ferreirim,I.M.A., Hoops and their implicational reducts, Algebraic
Methods in Logic and Computer Science, Banach Center Publications 28 (1993),
pp.219-230.
[2] Font,J.M. Rodrguez,A.J.and Torrens,A., Wajsberg algebras, Stochastica 8 (1984),
pp.5-31.
[3] Ono,H., Logics withoutcontractionrule and residuated latticeI, draft, 1999.
[4] Wronski,A., On varieties of commtative BCK-algebras not generated by their nite
members, Mathematica Japonica 30 No.2 (1985), pp.227-233.
