Japan Advanced Institute of Science and Technology

(1)

Japan Advanced Institute of Science and Technology

JAIST Repository

https://dspace.jaist.ac.jp/

Title

動的論理に関する研究

Author(s)

町田, 拓

Citation

Issue Date

2002‑03

Type

Thesis or Dissertation

Text version

author

URL

http://hdl.handle.net/10119/1575

Rights

Description

Supervisor:小野寛晰, 情報科学研究科, 修士

(2)

修士論文

動的論理に関する研究

指導教官

小野寛晰教授

北陸先端科学技術大学院大学情報科学研究科情報処理学専攻

町田拓

修了年月平成年月

(3)

第

章はじめに

背景

様相論理は古典命題論理では十分に説明することができない日常的な推論を扱うため、

「必然」、「可能」といった様相概念を表す演算子を導入し、その表現力を増したものであり、この様相演算子に対しての解釈を変えることにより、様々な論理体系が構築できる。

動的論理（）は、プログラム毎にその実行状態を表す様相演算子を導入した体系で、手続き型プログラム言語の仕様の記述やプログラムの正当性の検証のために用いられる。

計算機とプログラムに関する論理の研究は年代後半に^!と^"により始められた。動的論理は、^#$%による^!、^&による

等を経て、年に^'により導入された比較的新しい研究分野である。

動的論理を基礎とするいくつかの体系では未だ解決されていない重要な問題が存在し、それと同時に動的論理のソフトウェア科学への応用可能性の観点から、論理学と計算機科学の両面からの研究が盛んに行われている。

動的論理においては、繰り返し演算子の存在が論理体系を複雑にする。未解決問題の多くはこの繰り返し演算子に関わるものである。そのため、年に命題動的論理の繰り返し演算子の性質を少し弱め^#の^¾ の性質を持つ演算子に置き換えた論理が導入された⁽⁾。本研究では、この論理を中心に考察を進めていく。また対応する計算の体系の導入し、あわせてこちらの体系についても考察を進める。

(6)

本論文の構成

本論文は次のような構成を持つ。第章で動的論理、繰り返し演算子を置き換えた論理

およびその計算の体系の基本的な概念について述べる。第章では、⁽⁾で展開されているの完全性の証明の紹介をする。第章では、論理の完全性のカノニカルモデルを用いた証明を与える。続いて第章で体系の証明論的考察を行い、除去定理、補間定理の証明を示す。最後に第章で本研究のまとめを行う。

(7)

第

章

動的論理およびその周辺の体系

本章では動的論理および本研究で中心となる論理についての基本的な概念の説明を行う。

動的論理

動的論理は様相論理の一種である。様相論理は命題論理を拡張したもので「必然」、「可能」といった様相概念を表す演算子を導入してその表現力を増したものである。この様相演算子に対しての解釈により、時間論理、認識論理といった様々な論理体系がある。動的論理では、この様相演算子に対してプログラムの解釈を与えたものである。例えば、次のようなプログラムを考える。

*+ $!

*,+

これは、

にを代入する

の値がの値よりも小さいかを判定する

が成立する限りにを加える

というプログラムである。動的論理において、上の例にある^*および^*^,等のようなコンピュータに仕事をさせる命令をプログラムと呼び、のようなプログラム中における変数の値などの状態を表すものを論理式と呼ぶ。ここで、^*というプログラムを、^*^,というプログラムを、という論理式をとおく。すると、上

(8)

のプログラムは（連続的合成）、⁺ （繰り返し）、 ^-（テスト）の演算子を用いることにより、動的論理において

+.-+/

+-

と表すことができる。上のつの演算子に更に（非決定的選択）を加えることにより、動的論理においてどのような決定手続き型プログラムも作ることができる。

以下で基本的な動的論理である命題動的論理について紹介する。

定義動的論理において使用される演算子は、以下のものである。

論理式に関する演算子

./ 論理結合子

プログラムに関する演算子

./ + 合成演算子

./ 選択演算子

./

繰り返し演算子

論理式、プログラム双方に関する演算子

./ ( ) 必然演算子

.0/ - テスト演算子

以下では、論理式すべての集合を¹、命題変数すべての集合を¹、プログラムすべての集合を²、基本プログラムすべての集合を²とする。

定義動的論理の論理式およびプログラム動的論理において、論理式とプログラムは以下のように帰納的に定義される。

1

2

1ならば、 ¹

2ならば、⁺ ²

(9)

2 1ならば、^{( )} ¹

1ならば、^- ²

論理式の定義は^{( )} ¹という条件によりプログラムに依存し、プログラムの定義は

- 2という条件により論理式に依存する。したがって論理式とプログラムの定義は別々にすることができない。

1 2としたとき、主な合成プログラムおよび論理式の直観的な意味は以下のようになる。

( )：をどのように実行してもそのあとが真

+：の実行に続きを実行

：とのどちらか一方を非決定的に選択し実行

：を有限回（０回以上）実行

-：が真か偽かをテスト

可能性演算子は、 ^{( )}と定義される。また、主なプログラムは動的論理の枠組みのなかで以下のように定義できる。

%

* -

0

* -

0

3

*

-+

* .

-+

/

+.

/-

0 !

* 0 3

* -+-+

$!

*

* .-+ /

+-

* +$!

* +.-+ /

+-

動的論理の公理としては、以下のものをとる。

(10)

定義動的論理の公理系動的論理の公理は次のものからなる。

古典論理において恒真であるすべての論理式

( ). /.( )( ) /

( ). /( )( )

()( )()

( +)( )()

(-) . /

( )(

)(

)

(

).( )/(

)

また動的論理の推論規則は次のものからなる。

./

( )

例動的論理において以下は証明可能である。

(

)(

)

(

)

(

)( )

証明

定義の公理より⁽⁾⁽^).(⁾ ^{( )(}^)/ ⁽⁾⁽⁾。また公理より

(

).(

)( )(

)/。よって^./より⁽⁾⁽⁾⁽⁾。

定義の公理より明らか。

より^{( )(}⁾ ^{( )}。したがって定義の公理より⁽⁾ ^{( )(}⁾。ゆえに

(

)( )。

(11)

論理

命題動的論理において、繰り返し演算子の存在は論理体系を複雑なものにする。例えば、

ある論理式中に^{( )}というかたちのものが現れたとする。定義の⁽⁾^{( )(}⁾ という公理より、⁽⁾は^{( )(}⁾に置き換えられるが、^{( )(}⁾の⁽⁾は、同公理より再び^{( )(}⁾に置き換えられ、以下同じ事が続く。

このような繰り返し演算子が引き起こす複雑さを取り除き、しかも動的論理の持つ性質の多くを保持した体系として、文献⁽⁾において繰り返し演算子を様相論理^#の必然演算子^¾に置き換えた論理が導入されている。この論理は命題動的論理より弱い体系であるが、十分に強い表現力を持つ。^¾は各基本プログラム毎にあるが、以下では議論を簡単にするため基本プログラムを１つに固定する。本節では論理の基本的な説明を行う。

におけるプログラムおよび論理式の定義は、のそれに、

1ならば^¾ ¹ を加えたものである。

定義論理の公理系論理の公理は次のようなものからなる。

：古典論理のすべてのトートロジー

. /：^{( ).}^/^{.( )}^{( ) /}

.¾/：^¾. ^/^.¾^{¾ /}

.¾/：^¾

.¾/：^¾ ^¾¾

.¾ /：^¾ ^{( )}

また論理の推論規則は次のようなものからなる。

./

.

¾ /

¾

(12)

以下では文献⁽⁾に従ってについて説明する。まず、で使われる記号を定義する。

定義付値付き論理式 ¹であるとき、

4

を付値付き論理式という。ただし、はが真であることを、⁴ はが偽であることを表す。

1であるとき、

¾は^¾または^4¿を意味する

は^{( )}または⁴ を意味する

¾は^¿または^4¾を意味する

はまたは^{4( )}を意味する

上記の^¾^¾から様相演算子を除いたものを、添字を付けることにより表す。例えば、^¾ ^{* ¾}ならば、^¾

* である。また、を論理式の集合としたとき、

¾

*

¾

*

とする。以下に規則をあげる。

論理結合子に関する規則規則

. /

4規則

4. /

4 4

(13)

規則

. /

4規則

4. /

4

規則

./

4

4規則

4./

規則

. /

4

4規則

4. /

4

これら論理結合子に関する規則を適用したときの結果は、、⁴のような枝分かれしないものと、⁴、のような枝分かれをするものに分けられる。前者の形をしたものを論理式、後者を論理式とすると、それぞれに規則を適用した結果は、

の形に一般化できる。論理式には^.^/、^4.^/、^4.^/、⁴のつがあり、

それぞれに規則を適用した結果のは以下の表のようになる。

. /

4. / 4 4

4. / 4

4

同様に、論理式は^. ^/、^4.^/、^. ^/、であり、それぞれに規則を適用した結果のは以下の表のようになる。

. /

4. / 4 4

. / 4

4 4

(14)

以上は古典命題論理の体系の規則である。これに次の規則を加えたものが体系である。

¾規則

¾

¾規則

¾

規則

¾

¾および規則の^*^*は、これらの規則を適用することにより世界が変わることを意味している。実際のの証明においてはによって世界が変わったことを示す。

定義を以下のように定義する。論理式をにより証明するとき、

による証明は⁴から始まり、⁴ はである。

に論理式が現れたとき、つまり

のとき、これに規則を適用して得られた

もである。ただし、はこのにおいてより上に現れるすべての集合とする。

(15)

に論理式が現れた場合、つまり

に^¾が現れた場合、つまり

¾

のとき、これに^¾規則を適用して得られた

¾

もである。ただし、はこのにおいて^¾より上に現れるすべての集合とする。

に^¾が現れた場合、つまり

¾

のとき、これに^¾規則を適用して得られた

¾

もである。ただし、はこのにおいて^¾より上に現れるすべての集合とする。

(16)

にが現れた場合、つまり

¾

これらの手順で得られたもののみを論理式のという。また、の一番上にある⁴から一番下にある論理式までの一連の論理式の集まりを枝という。

定義以下の条件を満たすとき、の枝は閉じているという。

枝上に任意の論理式に対し、および⁴が存在する

枝上にが存在する

枝上に⁴が存在する

定義ある論理式に対して、⁴から証明が始まるにおいてすべての枝が閉じているとき、そのは閉じているといい、は証明可能であるという。

(17)

例 ^¾^¾.^{( )/}はで証明可能である。

4¾¾.( )/ ./

¾ ./

4¾. ( )/ ./

./

4./ 4¾.( )/ ./

¾ ./

4( ) ./

./

4( ) ./

¾ ./

4 ./

./

この例の場合、^./は証明すべき論理式であり、これに⁴規則を適用した結果が^./および^./である。^./に^¾を適用すると^./が導け、^./に⁴を適用すると^./、^./が導ける。^./に^¾規則を適用すると^./、^./が導ける（この場合、は^./〜^./、^¾は^./

であり、^./が^¾、^./が^¾ である）。^./に⁴規則を適用すると^./、^./が、^./に

規則を適用すると^./、^./が、^./に^¾ を適用すると^./がそれぞれ導ける。すると、これ以上の規則の適用はできない。ここで、各枝についてみてみると、左側の枝には⁵⁴（^./、^./）があるので、この枝は閉じた枝となる。また右側の枝上にも⁵⁴

（^./、^./）があるので、閉じた枝となる。ゆえにこのの枝はすべて閉じているので、論理式^¾ ^¾.^{( )/}はで証明可能である。

の

計算の体系

前節で論理のについて説明した。本節では、このに対するゲンツェン流の計算の体系を導入する。その前に基本となる命題論理の体系について説明する。

(18)

体系において、の形をしたものを式^{. /}と呼ぶ。

ただし、はでもよい。この式の直観的な意味は、「までを仮定すると

が導かれる」ということである。の推論規則は一般に

または

の形をしており、この推論規則を⁶とすると、を⁶の上式、を⁶ の下式と呼ぶ。以下では有限個（個を含む）の論理式を並べた列を⁷⁸等のギリシャ大文字で表す。体系

の始式および推論規則を以下にあげる。

始式

という形の式、ただしは任意の論理式

構造に関する推論規則

（^$%規則）

78

./

78

./

（規則）

8

78

./

78

./

（^9!規則）

7 28

./

78 :

./

（規則）

78 2:

728:

./

規則の論理式を、論理式という。

論理結合子に関する推論規則

(19)

7 8

./

78

./

78 78

78

./

78 78

78

./

78

./

78

./

78 2:

728:

./

78

./

78

7 8

./

78

./

定義証明図と終式証明図および終式を以下のように帰納的に定義する。

始式は証明図であり、その証明図の終式でもある。

はを終式とする証明図であるとする。さらに

または

がの推論規則の一つならば、

または

は証明図であり、その終式はである。

式を終式とするような証明図が存在するとき、はで証明可能であるといい、その証明図をの証明図という。

体系は、上記のに^¾と^{( )}に対する推論規則を付け加えることにより拡張したものである。

定義体系体系は古典命題論理の計算の体系に、

の^¾^¾の各規則に対応する以下の推論規則を付け加えたものである。

(20)

¾に対応

78

¾78 .

¾

/

¾に対応

¾7

¾7¾ .

¾

/

に対応

¾7:

¾7( ):( ) .

/

例において^¾ ^¾.^{( )/}は証明可能である。

¾ .

¾

/

¾ .

¾

/

¾ ( ) .

/

¾( )

. /

¾( )

./

¾ ¾. ( )/

.

¾

/

¾ ¾.( )/

./

(21)

第

章

体系

のに関する完全性

本章では⁽⁾による論理の、に関する健全性定理および完全性定理の証明を紹介する。この定理の証明は多少複雑であるため、続く第章において別のアプローチによる証明、すなわちフレームに関する完全性定理の証明を行う。

のセマンティクス

この節では、フレームという概念を用いて定められるのセマンティクスについて述べる。

定義フレームを空でない集合とし、^¾を上の二項関係とする。このときこれら３つの組^.^¾^/をフレームという。また、を可能世界の集合、そしておよび^¾を到達可能関係という。ただし、二項関係^¾には

¾は反射的かつ推移的

¾

なる条件があるものとする。

定義モデル ^.^¾^/をフレームとし、を各命題変数^!に対して ^.!/

となるような写像とする。このときをフレーム^.^¾^/上の付値といい、

.

¾

/をモデルという。このモデルに対し、の要素と論理式間の二項関係^*を以下のように帰納的に定義する。

*! .!/

(22)

*ではない

**ではない

* *かつ^*

* *または^*

* *ならば^*

* *かつそのときに限り^*

*( )

となる任意のに対し ^*

*¾

¾

となる任意のに対し ^*

関係^*は付値より一意に定まるので、以下ではは^*に置き換える。

定義恒真な論理式フレーム ^.^¾^/上の任意の付値^*および任意の^"

に対し^" ^* となるとき、論理式は ^.^¾^/で恒真であるという。モデル

.

¾

*/において、ある^# に対し^# となるとき、論理式は^.^¾^*/

において偽であるという。また、ある付値^*に対してが^.^¾^*/ で偽であるならば、はフレームで偽であるという。

の健全性定理

この節と次の節ではの健全性定理および完全性定理の証明を与える。

この証明は⁽⁾に述べられている証明を部分的に改良したものである。これを示すために、

２つの補助定理を示す。

定義 ^.^¾^*/をモデル、を付値付き論理式の集合とする。このとき、

に対して、任意ので^*となるとき、^*と書く。

補助定理 ^.^¾^*/をクリプキモデル、を付値付き論理式の集合とする。このとき、となる任意のに対し、

*ならば ^*^¾

¾

(23)

*ならば ^*^¾

*

¾ならば^*^¾

証明

* ならば、定義より任意のに対して ^* 。のかたちがならば、

定義よりとなる任意ので ^*。したがって ^*

、つまり ^*。また、^¾ ^¾。よって、任意の^¾ に対して、定義より ^*^¾。ゆえに ^*^¾

¾

。したがって ^*^¾

¾

。

¾

となる任意のをとる。^¾および^¾が推移的であることより、^¾ である。したがって、任意の^¾ で、^*^¾ならば ^*^¾、すなわち^¾ となる任意ので ^*^¾が得られるので ^*^¾。ゆえに ^*^¾。

仮定より^*^¾なので、定義よりとなる任意ので ^*^¾。^¾は反射的であるので。よって^*^¾。

定義充足可能論理式の集合に対し、あるモデルで^*となる世界が存在するとき、は充足可能であるという。の一つの枝上のすべての論理式の集合が充足可能であるとき、その枝は充足可能であるという。あるに対し、いくつかの枝が充足可能ならば、そのは充足可能であるという。

補助定理を充足可能なと仮定する。このとき、にひとつの規則を適用した結果得られるもまた充足可能である。

証明

$をの充足可能である枝とし、^$に規則を適用するとする。このとき、各規則毎に考察する。

規則を適用する場合（^$^*とし、これに規則を適用したものを^$ ^* とする） ^$は充足可能であるので、あるモデル^%^* ^.^¾^*/において

* かつ ^* となるが存在する。したがって定義より ^* かつ

*

。ゆえに^$は充足可能である。

(24)

規則を適用する場合（^$ ^*とし、これに規則を適用したものを^$ ^* および^$ ^* とする） ^$ は充足可能であるので、あるモデル^% ^*

.

¾

*/において ^* かつ ^* となるが存在する。したがって ^* または ^* である。ゆえに^$または^$のどちらかが充足可能である。

¾ 規則を適用する場合（^$ ^* ^¾ とし、これに^¾ 規則を適用したものを^$ ^*

¾

とする） ^$は充足可能であるので、あるモデル^%^*^.^¾^*/

において ^* かつ ^* ^¾となるが存在する。補助定理のより

*

¾

。ゆえに^$は充足可能である。

¾規則を適用する場合（^$^*^¾とし、これに^¾規則を適用したものを^$ ^*^¾^¾ とする） ^$は充足可能であるので、あるモデル^%^* ^.^¾^*/において

* かつ ^* ^¾となるが存在する。ここで ^* ^¾ならば定義より

¾

となるあるが存在して、 ^*^¾となる。また、補助定理のより^*ならば ^*^¾。したがって^$は充足可能である。

規則を適用する場合（^$ ^* とし、これに規則を適用したものを^$ ^*

¾

とする） ^$は充足可能であるので、あるモデル^%^*^.^¾^*/

において^*かつ^*となるが存在する。ここで^*ならば定義よりとなるある ^%が存在して、 ^* となる。また、補助定理の

、および ^¾より、 ^*ならば ^*^¾かつ ^* 。ゆえに^$は充足可能である。

定理の健全性定理がで証明できるならば、は任意のモデルで恒真である。

証明

4より証明が始まる閉じたがあると仮定する。⁴が充足可能であるとすると、補助定理より、任意の規則を適用したものも充足可能ある。しかし、閉じたは充足可能ではないので、これは矛盾。したがって、⁴は充足可能ではない。ゆえに任意の、任意のモデルで^*である。

(25)

のに関する完全性定理

この節ではに関する完全性定理の証明を行う。これを示すために、まずはのを定義し、それを用いてのモデル存在定理を示す。

の

ここではのの定義をし、またそれに関する重要な補助定理の証明を行う。

定義を付値付き論理式の集合族とする。が任意の

において以下の条件を満たすとき、という。

はと⁴を同時に含まない。また、は⁴、のどちらも含まない。

または ^&

¾

定義 ^' をとし、^' を付値付き論理式の集合とする。このとき、任意の ⁽ ^'に対し⁽ となるとき、は^' であるという。

補助定理をとし、をのすべての要素のすべての部分集合を含んでいるものとする。このときもである。また、が

'ならばも^'である。

証明

各定義毎に調べる。

がであることの証明

(26)

の要素はの部分集合であるが、は命題変数^!及び^!を持つような^#は含まない。したがっても同様にそのような^#を含まない。⁴、に関しても同様である。

を仮定する。このとき、となるが存在する。がであるので、。の構成及び

より、。

を仮定する。このとき、となるが存在する。がであるので、または。の構成及びより、または

。

¾

を仮定する。このとき、となるが存在する。^¾の定義より^¾ ^¾。がであるので、^¾^¾

。

の構成及び^¾^¾

¾

より、^¾^¾

。

を仮定する。このとき、となるが存在する。がであるので^¾

。いまであるので、

定義より ^¾ ^¾。の構成及び^¾

¾

より、^¾

。

¾

を仮定する。このとき、となるが存在する。が

であるので、 ^¾

。の構成及び^¾

¾

より、^¾

。

以上より、はである。

が^' であることの証明

( 'とする。このときとなるが存在。が^' であるので⁽ 。したがって、⁽⁽ 。ゆえには^' である。

補助定理を部分集合で閉じたとし、はすべての有限部分集合がに含まれる集合から成り立つとする。このとき、は

(27)

である。また、が^'ならばも^' である。

証明

であることの証明

ある命題変数^!および^!を含むが存在すると仮定する。このときこの２つの論理式からなる有限集合はに含まれるはずである。しかしも

なのでこれは矛盾。⁴に関しても同様。

とし、さらにを仮定する。このとき、⁾

となる有限集合⁾ が存在する。よりのすべての有限部分集合はに含まれる。よって、⁾は自身の部分集合ではない、つまり、

の少なくともどちらか一方が⁾に含まれるはずである。いま⁾ を⁾、⁾を⁾、⁾ を⁾

とする。このとき、

)

はの部分集合であるが、⁾

)

のうちのいずれか、またはすべてが成り立つ。ここで⁾ ^*⁾ )

)

とすると、⁾はの有限部分集合でありより⁾ 。が

、 ⁾ より⁾ ⁾ ⁾ 。は部分集合に関して閉じているので⁾ 。これは上の三つのどれかがなりたつことと矛盾。したがって。

とし、さらにかつを仮定する。このとき、より⁾ となる有限集合⁾ が存在。

よりのすべての有限部分集合はに含まれる。よって、⁾ は自身の部分集合でない、つまり、 ⁾。いま⁾ を⁾とする。このとき、⁾

)

。同様に⁾ となる⁾ が存在し、

)

を⁾とすると、⁾

)

。ここで⁾ ^*⁾ )

とすると、⁾ はの有限部分集合でありより⁾ 。が

、 ⁾ なので⁾ または⁾ 。は部分集合に関して閉じているので⁾

または⁾

、これは矛盾。したがってまたは。

(28)

¾

とし、さらに^¾ ^¾

を仮定する。このとき、⁾

¾

となる有限集合⁾ が存在。^¾ より⁾は^¾自身の有限部分集合でない、つまり^¾

)

。いま⁾^¾

を⁾とする。このとき、⁾

¾

)

¾

。ここで⁾ ^* ⁾

¾

とすると、⁾ はの有限部分集合でありより⁾ 。がなので

)

¾

。⁾ の構成より⁾^¾ ^*⁾^¾。また⁾のすべての要素が^¾に属するので⁾

*)

¾

。したがって⁾^¾ ^*⁾、これは矛盾。ゆえに^¾^¾

。

とし、さらに^¾

を仮定する。このとき、

)

¾

となる有限集合⁾ が存在。このとき

が⁾ に入るか否かの２つの場合に関して

./

) の場合。このとき⁾ ^¾。ここで ⁾ ^*^{( )} ^.)

/.)

¾

/とすると、⁾ 、より⁾ 。⁾ は有限なので⁾ 。より⁾ 、したがって ⁾ 。

がなので⁾

。は部分集合に関して閉じているので⁾ 、これは矛盾。ゆえに^¾

。

./

) の場合。⁾

を⁾とする。このとき、⁾ は有限で⁾

¾

。^/の場合と同様に⁾

が得られる。これは矛盾。

¾

とし、さらに^¾

を仮定する。このとき、⁾ ^¾

となる有限集合 ⁾ が存在。より、⁾ は自身の有限部分集合であり得ない。つまり^¾

)

。いま⁾ ^¾

を⁾ とする。このとき、

)

¾

。ここで⁾ ^* ⁾ ^¾とすると、⁾ は有限かつ

) 。またより⁾ ^¾

。は部分集合に関して閉じているので⁾^¾

、これは矛盾。したがって^¾

。

が^' であることの証明

( ' を仮定する。よりのすべての有限部分集合はに属する。

ここで⁾ を⁾ であるような有限集合とすると⁾ かつが^' であることより⁾⁽ 。ゆえに⁽のすべての有限部分集合はに属する。

定義集合族は、となる任意のに対し、の任意の有限部分集合がに属するときかつそのときに限り、であるという。

命題任意の（^'）はな

（^'）に拡張できる。

(29)

証明

補助定理およびから導ける。

上の結果から、ツォルンの補題を用いて次のことが証明できる。

命題をとする。このとき、に属する任意の集合に対し

となるような極大集合が存在する。

のモデル存在定理

ここではのモデル存在定理の証明を行う。この定理はの完全性定理を証明するときに使われる。いまをとする。命題より、となる

かつ³ ^!であるようなが存在する。

定義の固有モデル^.

¾ *

/ を以下のように定義する。

：の極大集合全体の集まり

*

に対し、^* *

*

に対し、^*¾ *

¾

、命題変数^!に対し、^* ^! ^! 補助定理以下が成り立つ。

任意の^* で^*¾

*

任意の^* で¾

*かつ^*¾

ならば¾

任意の^* で^*

ならば^*¾

証明

定義より^*^¾^*、したがって^*¾

*。

¾

*かつ^*¾

であると仮定する。すなわち、^¾ ^*^*^¾ ^*。定義より^" ^#

"

¾

#

¾であるので、^¾¾ ^*^¾。また、^"^¾¾ ^*^"^¾であるので、^¾ ^*^¾ 。したがって、^¾ 。ゆえに¾

。

(30)

*

を仮定し、さらに任意ので^¾ ^*とする。このとき、^.¾^/より^{( )} ^*。

*

より。したがって^*¾ 。

定理のモデル存在定理がであるとする。が

ならばは充足可能である。

証明

をとし、さらにを、つまりを仮定する。このときが充足可能であることを示す。ここで、定義で定めたモデルを考える。

このモデルは補助定理よりモデルである。以下では

任意の、付値付き論理式⁽に対し、⁽ ならば^*⁽

が成り立つことを示す。この付値付き論理式⁽のサイズによる帰納法により証明する。

基底段階

(のサイズがのとき、⁽は^!または^4!である。ただし、^!は命題変数。このとき、

! *

!、よって^*^!

4! ! 、つまり^* ^!、よって^*^!

帰納法の仮定

任意の以下のサイズの各付値付き論理式において、⁽ ならば

*( とする。

(のサイズを⁺とする。⁽の形により以下のように場合分けする。

( * のときがであることよりならば

。よってが極大であることより。ゆえに帰納法の仮定より^*かつ^*。したがって^*。

( *のときがであることよりならばまたは。よってが極大であることよりまたは。ゆえに帰納法の仮定より^*または^*。したがって^*。

( *

¾ のときがであることより^¾ ならば^¾

¾

。ここでにおいて^¾^¾

を極大に拡張したものをとする。このとき。^¾

および^¾のサイズが^¾より小さいので帰納法の仮定より

*

¾

。また^¾より^¾。ゆえに^*^¾。

(31)

( *

のときがであることよりならば

¾

。ここでにおいて^¾

を極大に拡張したものをとする。このとき。

およびのサイズがより小さいので帰納法の仮定より ^*。またより。ゆえに^*。

( *

¾のとき ^¾（つまり^¾ ）となる任意のをとを考える。

¾

ならば^¾ ^¾。^¾ より^¾ 。ゆえにがであることより ^¾

。はにおいて極大であるので^¾

。帰納法の仮定より ^* ^¾。よって^¾となる任意ので ^* ^¾。以上より

* 。

( *

のとき（つまり）となる任意のを考える。

ならばの定義より

。より。帰納法の仮定より ^*。したがってとなる任意ので ^*。ゆえに^*。

の完全性定理

定義付値付き論理式の集合は、の閉じたが存在しないとき無矛盾であるという。

補助定理をすべての無矛盾集合からなるクラスとする。このときは

である。

証明

とする。がある命題変数^!と^!を同時に含むと仮定すると、の閉じたが存在する。よっては無矛盾ではない、つまり。これは矛盾。したがってはある命題変数^!と^!を同時に含まない。⁴に関しても同様。

を仮定し、とする。このとき

$

Japan Advanced Institute of Science and Technology