命題論理 · 命題様相論理の Hilbert 流の演繹体系の完全性について
de@ics.nara-wu.ac.jp) 2014/06/20 第 1 版
NIDE, Naoyuki (nitoma
2017/01/12 第 2 版
2017/02/05 第 2.1 版
2017/09/27 第 2.4 版

1に括弧をつけて A ⊃ (B ⊃ C) と書く。その他の二項演算

はじめに子は左結合とする。
本稿は、[2] の 5.5 節 (命題信念様相論理) への補足を意図して書かれている。具体的には、その節で定理 5.5 として証明なしに述べられている、命題信念様相論理 (命題様

2

命題論理

2.1

Hilbert 流の演繹体系

相論理体系 KD45 に相当) の Hilbert 流の演繹体系1 の完全性に対し、証明を与えることを目的とする。

Hilbert 流の演繹体系については、完全性の証明も、ま命題 (非様相) 論理の Hilbert 流の演繹体系を導入する。

た、与えられた論理式の証明を作り出すことも、直感的には行いにくい。一方、2.3 節で述べるシーケント計算と2.1.1呼ばれる演繹体系は、特に命題論理/命題様相論理につい公理

2ては、完全性の証明は、極めて直感に沿った形で行える 。

「:」の左はそれぞれの公理の名前である。

それは、論理式 A が証明可能でないと仮定すると、自然

Ax1 : A ⊃ (B ⊃ A)

な形で、A を偽にする真理値割り当て (命題論理の場合)、
ないしはクリプキ · モデル (命題様相論理の場合) が作れ

Ax2 : (A ⊃ (B ⊃ C)) ⊃ ((A ⊃ B) ⊃ (A ⊃ C))

ることによる。また、それと同じ考え方で、論理式の証

Ax3 : (¬A ⊃ ¬B) ⊃ ((¬A ⊃ B) ⊃ A)

明を作り出すアルゴリズムの存在も自然に示せる [1]。
そこで本稿では、シーケント計算による証明を、Hilbert
流の演繹体系での演繹に変換することによって、命題論理

2.1.2

規則

や命題様相論理 K, KD45 の Hilbert 流の演繹体系における規則の横線の上の論理式の集合をその規則の「前提」、

完全性の証明や、同体系での論理式の証明を作り出す方下の論理式を「結論」と呼ぶ。横線の右はその規則の名法が得られることを示すという方針をとる。特に、Hilbert

前である。

流での命題様相論理 KD45 の演繹体系の完全性の証明は、

A

各種書籍にも意外に取り上げられていないので、それを補うことをも目的とする。

A⊃B
MP
B

以下、2 節では命題 (非様相) 論理、3 節では命題様相
論理 K の体系について述べ、次いで 4 節で命題様相論理

2.1.3

演繹

KD45 について述べる。
公理と Γ から規則を使って A が導けることを Γ ⊢ A と書く。正確に言うと、Γ ⊢ A とは、論理式をノードとし、以後、A, B, · · · は論理式、Γ, ∆, · · · は論理式の multi

set を表す。また、古典 (非様相) 論理記号は ⊃, ¬ のみとし、A ∧ B は ¬(A ⊃ ¬B) の、A ∨ B は ¬A ⊃ B の、それぞれ略記とする。論理記号の優先順位は、単項演算子 ·かつ以下を満たす有限木が存在することである。

1. 根は A
2. 葉は Γ の要素あるいは公理∧ · ∨ · ⊃ の順に高いとする。⊃ は右結合とするが、しばしば、紛れにくいよう A ⊃ B ⊃ C のような場合も明示的

3. 葉でない任意のノード N に対し、N を結論とし、
N の子ノードの集合を前提とする規則が存在する

1 「Hilbert 流」の演繹体系とは、[2] の 2.5 節 (命題論理の公理と推論規則) や 5.1.5 項 (体系 K)、5.5.4 項 (命題信念様相論理の体系) のよ
うに、公理と推論規則から定理となる論理式を演繹する体系のことを指す。なお、[2] では「演繹体系」を「公理系」と呼んでいるが、本稿では「演繹体系」で統一する。
2 何をもって「直感的」「直感に沿った」と呼ぶかには個人差もあろうが、少なくとも筆者には、Hilbert 流よりもシーケント計算に対する完全性の証明の方がずっと直感的でわかりやすいものと感じる。

また、その木を Γ からの A の「演繹」、あるいは紛れがなければ単に「演繹」と呼ぶ。特に、∅ からの A の演繹を A の「証明」と呼ぶ。
なお、今のところ規則は MP だけである。

1

• 木のノードが 1 つだけなら、そのノード B は Γ の要
素か公理か A である。B = A の場合は A ⊃ A が証

しばしば、論理式の multi set と論理式の列を適切に同一視する。すなわち、{A1 , · · · , An } ⊢ A のことを A1 , · · · ,An ⊢ A と (特に、∅ ⊢ A のことを ⊢ A と) 書いたり、Γ ∪ {A1 , · · · , An } ⊢ B のことを Γ, A1 , · · · , An ⊢ B と書

明でき、それ以外の場合は B から Weak で A ⊃ B

いたりする。

演繹が作れる。

を導けるため、いずれの場合も Γ から A ⊃ B への

⊢ A のとき A を定理という。

• 木のノードが 2 つ以上の場合、木の根は B である。
規則は MP だけであるため、ある論理式 B ′ が存在して、Γ, A から B ′ への演繹の木と、Γ, A から B ′ ⊃ B

2.2

演繹定理

への演繹の木があり、B の子ノードは B ′ と B ′ ⊃ Bである。帰納法の仮定から、Γ から A ⊃ B ′ への演

命題論理の Hilbert 流の演繹体系に対する、演繹定理を繹の木と、Γ から A ⊃ (B ′ ⊃ B) への演繹の木が存示す。

在する。それらの根から MP2 で A ⊃ B を導けることから、Γ から A ⊃ B への演繹も存在する。

2.2.1 補助規則その 1
証明には、規則が MP だけであることと、ID が定理で以下は、本来の規則と同様、規則として用いることがあることが使われている。従って、MP 以外の規則 (補助できる。これらを以降では補助規則と呼ぶ。横線の右側

規則は除く) を持つ演繹体系では、定理 2.1 の右から左はその補助規則の名前である。

は必ずしも成り立たない (例えば 3 節の命題様相論理で、A⊃B

A ⊢ □ A だからといって ⊢ A ⊃ □ A とはならない)。また、公理が少なくて ID を証明できない場合も、右から左

A
Weak
B⊃A

A ⊃ (B ⊃ C)
MP2
A⊃C

は必ずしも成り立たない。

A⊃B B⊃C
MP1
A⊃C

この証明は、「Γ, A からの B の演繹」を与えて「Γ からの A ⊃ B の演繹」を作るアルゴリズムの存在も示して

上 2 つは公理と MP からすぐ、MP1 は上 2 つから得ら

いる。

れる。

2.3
2.2.2 補助定理その 1

シーケント計算

以下、シーケント計算による演繹体系を導入する。本稿でのシーケント計算の定義は基本的に [1] のものを踏襲

定理のうち、公理と同様に用いるものを以降では補助する。

定理と呼ぶ。次のものは補助定理である (「:」の左は補助

A1 , · · · , Am → B1 , · · · , Bn の形をしたもの (但し 0 ≤ m,
0 ≤ n で、A1 , · · · , Am , B1 , · · · , Bn は論理式) をシーケン定理の名前)。この式は後に演繹定理の証明で使われることに注意。

トという。シーケントの「→」の左のみ、または右のみのID : A ⊃ A

順番を入れ替えたものは、元のシーケントと同一視する。

証明は以下から得られる (B は任意でよい)。

A ⊃ (B ⊃ A)

2.3.1

A ⊃ ((B ⊃ A) ⊃ A)
MP2
A⊃A

イニシャルシーケント「→」の左と右に同一の論理式があるシーケントをイニシャルシーケントという。

2.2.3 演繹定理

2.3.2

定理 2.1 Γ ⊢ A ⊃ B iff Γ, A ⊢ B

シーケント計算の推論規則

シーケント計算の各推論規則は、横線の上にシーケン

証明 左から右へは MP があるので明らか。右から左へ

トが 0 個以上、下にシーケントが 1 個という形をしていは、Γ, A から B への演繹の木のノード数に関する帰納法

る。線の上のシーケントをその規則の「前提」、下のシーによる。

ケントを「結論」と呼ぶ。

2

命題論理のシーケント計算の推論規則は以下のもので恒真であり (各推論規則につき、結論が恒真なら前提も恒ある。論理記号が ⊃ と ¬ だけなので、これらに対する規真であることが示せるため)、かつ論理オペレータは k 個

則しかない。

以下なので、帰納法の仮定から証明可能である。従って

Γ → ∆, A Γ, B → ∆⊃左Γ, A ⊃ B → ∆Γ → ∆, A¬左Γ, ¬A → ∆S も証明可能である。恒真な論理式が証明可能であるこΓ, A → ∆, B
⊃右
Γ → ∆, A ⊃ Bとは、このことからすぐ従う。

Γ, A → ∆¬右Γ → ∆, ¬A

また、任意に与えたシーケント S が証明可能か否かは
以下のようにして求まる。S 内に論理オペレータ (⊃, ¬)いずれも、結論のシーケントは「→」の左か右に ⊃ あるが 1 つ以上あれば、S を結論とする推論規則が存在し、そいは ¬ があり、前提のシーケントではその ⊃ あるいは ¬の前提はいずれも論理オペレータの個数が S より少ない。

が外れる形となっている。さらに、「→」の左か右に ⊃ か

それらのシーケントに対し同様の過程を繰り返すと、論¬ が 1 つ以上ある任意のシーケント S に対し、S を結論

理オペレータの個数が減っていき、いずれは 0 個になる。

とする推論規則が必ず存在する。これらの性質は 2.3.3 節

そのようにして得られた論理オペレータ 0 個のシーケンで使う。

トが全てイニシャルシーケントであれば S は証明可能であり、またイニシャルシーケントでないものが 1 つでも証明可能なシーケントを以下のように定義する。

あればそのシーケントは恒真ではないので、S も恒真で• イニシャルシーケントは証明可能はなく、従って証明可能ではない。

• 推論規則の前提のシーケントが全て証明可能ならば結論のシーケントも証明可能

2.4 Hilbert 流の演繹体系の完全性

また、論理式 A が証明可能であるとは、シーケント → Aが証明可能であることとする。

まず、Hilbert 流の演繹体系での追加の補助規則をいく
つか導入し、続いて、シーケント計算での証明から Hilbert
流演繹への変換を示すことにより、Hilbert 流の演繹体系

2.3.3 シーケント計算の完全性その他の完全性を示す。
シーケント計算の健全性 · 完全性は容易に示せる。また、シーケントを (あるいは論理式を) 与えて、それが証明可能ならその証明を実際に与え、さもなければ証明可能で2.4.1

ないと答えるアルゴリズムの存在も容易に知れる。詳細は [1] を参照。以下に概略を示す。

Hilbert 流の演繹体系での補助規則その 2¬A ⊃ ¬B ¬A ⊃ B
PD1
A(命題論理の意味論が定義済みであるとして) シーケン
ト A1 , · · · , Am → B1 , · · · , Bn の真理値を、論理式 ¬A1 ∨

¬B B
IN
A

· · · ∨ ¬Am ∨ B1 ∨ · · · ∨ Bn の真理値と同じと定義し、またこの論理式が恒真のとき、元のシーケントも恒真という。

¬¬A
DN
A

¬A ⊃ ¬B
A

B

PD2

A ⊃ ¬B A ⊃ B
PD3¬A

PD1 は公理と MP から、PD2 と IN の 2 つは PD1 と Weak

すると、イニシャルシーケントは恒真であり、また、シーからすぐ。DN は下記から得られる。

ケント計算の推論規則の前提が全て恒真ならば結論も恒

¬¬A
ID
Weak
¬A ⊃ ¬¬A¬A ⊃ ¬A
PD1
A

真である。これより、証明可能なシーケントは恒真であり、よって証明可能な論理式も恒真である。
一方、恒真なシーケントが証明可能であることを示すには、シーケント内の論理オペレータ (⊃, ¬) の個数 n に

演繹定理により、IN および DN は補助定理 ¬B ⊃ (B ⊃ A),

関する帰納法による。n = 0 でかつ恒真なシーケントは¬¬A ⊃ A としても使える。このことから、PD3 も以下のようにして得られる。

イニシャルシーケントであるので、証明可能である。次に n ≤ k の場合を仮定し、n = k + 1 でかつ恒真なシーケ

補助定理 (DN)
補助定理 (DN)¬¬A ⊃ A A ⊃ B¬¬A ⊃ A A ⊃ ¬B
MP1
MP1¬¬A ⊃ ¬B¬¬A ⊃ B
PD1
¬A

ント S があるとすると、S の → の左か右に論理オペレー
タ (⊃, ¬) が少なくとも 1 つあるため、S を結論とする推論規則が必ず存在する。その推論規則の前提はいずれも

3

2.4.2 シーケント計算での証明から Hilbert 流演繹への変換

また、以上の証明からは、シーケント S の証明が与えられていれば、S の Hilbert 流演繹を具体的に作れることもわかる。

以下、Γ の論理式の 1 つ 1 つに ¬ を付けたものを ¬Γ と書く (例えば Γ = {p, p ⊃ q} ならば ¬Γ = {¬p, ¬(p ⊃ q)})。

系 2.3 命題 (非様相) 論理の Hilbert 流の演繹体系は健全か

Hilbert 流の公理のうち適当に選んだ 1 つを T とする。
シーケント S = Γ → ∆ に対し、Hilbert 流の演繹体系でつ完全。

の Γ, ¬∆ から ¬T への演繹が存在するならば、それを「S証明 健全性は容易。完全性を示すため、論理式 A が恒真の Hilbert 流演繹」と呼ぶことにする。

とする。シーケント計算の完全性より、シーケント → A

定理 2.2 任意の証明可能なシーケント S に対し、S のする。すなわち ¬A ⊢ ¬T である。演繹定理と PD2、おHilbert 流演繹が存在する。

よび T が公理であることから ⊢ A となる。

は証明可能である。よって、→ A の Hilbert 流演繹が存在証明 イニシャルシーケントの Hilbert 流演繹が存在する
以上からはさらに、恒真な論理式 A に対し、A の Hilbert

こと、および、シーケント計算の各推論規則について、前流体系での証明を具体的に作れることもわかる。

提のシーケントの全てに Hilbert 流演繹が存在するならば結論のシーケントにも Hilbert 流演繹が存在することを示せばよい。

• S がイニシャルシーケント Γ, A → ∆, A の場合、Sの Hilbert 流演繹は以下のように作れる (Γ, A, ¬∆,¬A ⊢ ¬T )。
A ¬A
IN
¬T

A⊃B

B

Hilbert 流の演繹体系(例えば Γ = {p, p ⊃ q} ならば □ Γ = {□ p, □(p ⊃ q)})。

3.1.1(Γ, A ⊃ B, ¬∆ ⊢ ¬T )。T が公理であることに注意。
PD2

3.1

命題様相論理 K の Hilbert 流の演繹体系を導入する。以¬∆, ¬A ⊢ ¬T および Γ, B, ¬∆ ⊢ ¬T ) 場合、演繹定理より Γ, ¬∆ ⊢ ¬A ⊃ ¬T および Γ, ¬∆ ⊢ B ⊃ ¬Tであり、以下により結論の Hilbert 流演繹を作れるT

命題様相論理 K下、Γ の論理式の 1 つ 1 つに □ を付けたものを □ Γ と書く• ⊃左の前提それぞれに Hilbert 流演繹が存在する (Γ,¬A ⊃ ¬T
A

3

MP
¬T

B ⊃ ¬T

公理

命題論理の公理に以下を加えたもの。

K : □(A ⊃ B) ⊃ (□ A ⊃ □ B)
MP

正確に言うと、命題論理の公理の A, B, C を命題様相論理の論理式で置き換えたものも公理 (例えば □ A ⊃ (□ B ⊃• ⊃右の前提に Hilbert 流演繹が存在する (Γ, A, ¬∆,□ A) がそう) である。

¬B ⊢ ¬T ) 場合、以下により結論の Hilbert 流演繹
を作れる (Γ, ¬∆, ¬(A ⊃ B) ⊢ ¬T )。
¬(A ⊃ B)
補助定理 (IN)Weak¬A ⊃ ¬(A ⊃ B)
¬A ⊃ (A ⊃ B)
PD1
A

3.1.2

規則

命題論理の規則に以下を加えたもの。

¬(A ⊃ B)Weak
B ⊃ ¬(A ⊃ B)
B ⊃ (A ⊃ B)
PD3
¬B

A
Nec
□A
演繹の定義は 2.1.3 節と同じ。

• ¬左の前提に Hilbert 流演繹が存在する場合、結論の以降では、演繹のうち、途中の過程で「定理でない論理

Hilbert 流演繹はそれと同じである。

式 A に対し Nec を適用」していないもの (すなわち、演• ¬右の前提に Hilbert 流演繹が存在する (Γ, A, ¬∆ ⊢¬T ) 場合、DN により結論の Hilbert 流演繹を作れ

繹の木に □ A の唯一の子ノード A でかつ定理でないものが存在しないもの) を「正規演繹」と呼ぶことにし、Γ か◦る (Γ, ¬∆, ¬¬A ⊢ ¬T )。

ら A への正規演繹があるとき Γ ⊢ A と書く。

4

• Nec の前提に Hilbert 流正規演繹が存在する (A1 , · · · ,An , ¬A ⊢◦ ¬T ) 場合、演繹定理および PD2 より A1 ,3.1.3 演繹定理
演繹定理は制限付きでしか成り立たない。
◦· · · , An ⊢◦ A となり、さらに演繹定理から ⊢◦ A1 ⊃A2 ⊃ · · · ⊃ An ⊃ A、Nec から ⊢◦ □(A1 ⊃ A2 ⊃◦定理 3.1 Γ ⊢ A ⊃ B iff Γ, A ⊢ B· · · ⊃ An ⊃ A) を得る。
◦
ここから公理 K と MP を用いて □ A1 ⊢ □(A2 ⊃· · · ⊃ An ⊃ A) を得、さらに同様の過程を繰り返証明 「演繹」が「正規演繹」に変わること以外、定理 2.1の証明とほぼ同様。特に、規則 Nec が加わったため、場
合分けの中に、木の根 B が □ B ′ の形をしていて、B の′◦すことで □ A1 , · · · , □ An ⊢ □ A を得る。IN から◦

唯一の子ノードが B である場合が加わる。この場合 ⊢ B◦□ A1 , · · · , □ An , ¬ □ A ⊢ ¬T となり、従って Necの結論にも Hilbert 流正規演繹が存在する。

◦

なので、Weak により ⊢ A ⊃ B でもある。従って Γ から

A ⊃ B への正規演繹が存在する。

また、以上から、シーケント S の証明が与えられてい

3.2

れば、S の Hilbert 流正規演繹を具体的に作れることもわ

シーケント計算かる。

命題様相論理 K のシーケント計算による演繹体系を導入する。シーケント、イニシャルシーケントの定義は 2.3

系 3.3 K の Hilbert 流の演繹体系は健全かつ完全。

節と同じ。

証明 系 2.3 と同様。特に、論理式 A が恒真の場合、シーケント → A の Hilbert 流正規演繹が存在することに注意。

3.2.1 シーケント計算の推論規則

また、恒真な論理式 A に対し、A の Hilbert 流体系での証明を具体的に作れることもわかる。

命題論理のシーケント計算の推論規則に以下を加えた
もの。

Γ→A
Nec
□Γ → □AΓ→∆WeakΓ, Γ′ → ∆, ∆′シーケントや論理式が証明可能であることの定義も 2.3.2節と同じ。
体系 K に関しても、シーケント計算の健全性や完全性

4

命題様相論理 KD45

4.1

Hilbert 流の演繹体系

命題様相論理 KD45 の Hilbert 流の演繹体系は、命題様

は、命題論理のシーケント計算よりは少し難しくなるも相論理 K の公理に以下を加えたものである。

のの比較的容易に示せる。また、シーケントを (あるいは論理式を) 与えて、それが証明可能ならその証明を実際にD : □ A ⊃ ¬ □ ¬A

与え、さもなければ証明可能でないと答えるアルゴリズ

4: □ A ⊃ □ □ A

ムの存在も示せる。これらについても [1] 参照。

5: ¬ □ A ⊃ □ ¬ □ A

3.3

規則は命題様相論理 K と同じ。演繹の定義も K と同じで

体系 K での Hilbert 流の演繹体系の完全性ある。演繹定理は定理 3.1 と同じ形で成り立つ。

Hilbert 流の公理のうち適当に選んだ 1 つを T とする。
シーケント S = Γ → ∆ に対し、Hilbert 流の演繹体系での Γ, ¬∆ から ¬T への正規演繹が存在するならば、それ4.2

シーケント計算を「S の Hilbert 流正規演繹」と呼ぶことにする。
命題様相論理 KD45 のシーケント計算による演繹体系
定理 3.2 任意の証明可能なシーケント S に対し、S のを導入する。特に、KD45 での完全性に関しては、取り上

Hilbert 流正規演繹が存在する。

げている書籍が (Hilbert 流についてと同様、シーケント計

証明 定理 2.2 とほぼ同じ。特に、算についても) 少ないので、ここにシーケント計算の完全性も示す。

• Weak の前提に Hilbert 流正規演繹が存在する場合、シーケント、イニシャルシーケントの定義は 2.3 節と結論に Hilbert 流正規演繹が存在することは明らか。

同じ。

5

• ここで、mi > 0 または ni > 0 となるような i が 1つでもある場合は、そのような i のうち 1 つを選び、4.2.1 シーケント計算の推論規則
推論規則は、命題様相論理 K のシーケント計算の推論

Si′ を改めて S ′ と置いて (従って m や n もそれぞれ
mi , ni ほど増える)、繰り返しの先頭に戻る。さも規則から Nec を取り除き、以下を加えたものである。

□ Γ, Γ → □ ∆, □ A, A
Nec45
□ Γ → □ ∆, □ A□ Γ, Γ →NecD45□Γ →なければ繰り返しを終了。
この繰り返しは有限回で終了する。すなわち、→ の左右の □ A の形のシーケントがいつまでも増え続けることはない。なぜなら、→ の左右に来うる論理式は、S に現れ

4.2.2 シーケント計算の健全性 · 完全性

る論理式の部分論理式に限られ、それは有限通りしかな
いためである。

健全性は容易。以下に完全性を示す。

続いて以下のようなクリプキ · モデル M = ⟨W, R, V ⟩定理 4.1 シーケント S が証明可能でないならば、世界間を作る。すると、R は serial, transitive, Euclidean である。

の到達可能関係が serial, transitive および Euclidean であっ

Si′ は証明可能でないので、Si′ の → の左右に同じ原子命てかつ S を偽とする3 クリプキ · モデル4 が存在する。

題が現れることはない。

証明 以下の過程では、シーケントの → の左同士あるい• W = {w0 , w1 , · · · , wn } (n > 0 の場合) または W ={w0 , w1 } (n = 0 の場合)は右同士に同一の論理式が複数現れた場合、暗黙のうちに
随時 Weak を逆向きに適用し、→ の左同士あるいは右同• R = {⟨wi , wj ⟩ | j > 0} すなわち、どの世界から士に同一の論理式が複数現れないように保つものとする。

も w0 以外の全ての世界が到達可能⊤(真) if Si′ の → の左に p が現れる
• V (wi , p) = ⊥(偽) if Si′ の → の右に p が現れる

どちらでもいい if 上記以外

S = S0 と置き、S0 に対し、⊃左, ⊃右, ¬左, ¬右 を可能
な限り逆向きに適用すると、少なくとも 1 つ、p1 , · · · , pk ,□ A1 , · · · , □ Am → q1 , · · · , qℓ , □ B1 , · · · , □ Bn の形 (ここで k ≥ 0, m ≥ 0, ℓ ≥ 0, n ≥ 0 であり、p1 , · · · , pk , q1 , · · · ,qℓ は原子命題) の、証明可能でないシーケントが得られすると、各 i (i ≥ 0) について、Si から Si′ を導く過程でる。これを S0′ とする。

経由する各シーケント (Si , Si′ も含む) の → の左に現れる

S ′ = S0′ と置いて、以下を繰り返す。

論理式はモデル M の世界 wi で真、→ の右に現れる論理′• n > 0 の場合、S に Weak と Nec45 を逆向きに適用して、n 個のシーケント □ A1 , · · · , □ Am , A1 , · · · ,Am → □ B1 , · · · , □ Bn , Bi (1 ≤ i ≤ n) を得る。これ

式は wi で偽となる。このことは、論理式の構造に関する帰納法で以下のように示せる。

• 原子命題については、V (wi , p) の作り方から明らか。

らを S1 , · · · , Sn とする。また、n = 0 の場合は、S ′• → の左の A ⊃ B の形の論理式は、Si′ に至るまでにどこかで ⊃左 を適用され、→ の右の A か → の左の B のどちらか一方が、Si′ に至る過程に現れる。

に Weak と NecD45 を逆向きに適用し、1 個のシー
ケント □ A1 , · · · , □ Am , A1 , · · · , Am → を得て、これを S1 とする。これらはいずれも証明可能でない。

前者が現れる場合は、帰納法の過程から A が wi で• 各 Si (n > 0 の場合は 1 ≤ i ≤ n、n = 0 の場合は
i = 1) に対し、⊃左, ⊃右, ¬左, ¬右 を可能な限り偽、従って A ⊃ B は wi で真。後者が現れる場合も同様。

逆向きに適用すると、i 毎に少なくとも 1 つ、pi1 ,• → の右の A ⊃ B 、→ の左右の ¬A の形の論理式に· · · , piki , □ A1 , · · · , □ Am , □ Ai1 , · · · , □ Aimi → q1i ,· · · , qℓii , □ B1 , · · · , □ Bn , □ B1i , · · · , □ Bni i の形 (ここついては上と同様。

• → の左の □ A の形の論理式は、S ′ の → の左にも現れているため、各 Sj (j > 0) の → の左に A が現れている。帰納法の仮定から各 wj で A が真、よっで ki ≥ 0, mi ≥ 0, ℓi ≥ 0, ni ≥ 0 であり、p や q に添字の付いたものは原子命題) の、証明可能でない
シーケントが得られる。これら (i 毎に 1 つ選ぶ) を

Si′ とする。Si′ の → の左右の、□ A の形のシーケン
トは、S ′ に比べて減ることはないことに注意。

て wi で □ A は真。

• → の右の □ A の形の論理式は、S ′ の → の右にも現れているため、ある Sj (j > 0) の → の右に A が現れている。帰納法の仮定から wj で A が偽、よっ3 シーケント A , · · · , A
m → B1 , · · · , Bn の真理値は、論理式 A1 ,1· · · , Am が全て真で B1 , · · · , Bn が全て偽のときに限り偽、それ以外の場合は真と定義する。これは 2.3.3 節での定義と同等である。
4 クリプキ · モデルの定義は [2] による。

て wi で □ A は偽。

6

証明 系 3.3 と同様。

従って S0 は (すなわち S は) w0 で偽である。
系 4.2 KD45 のシーケント計算は完全である。

また、KD45 に対しても、恒真な論理式 A に対し、A の証明 論理式 A が証明可能でないならば、シーケント → A

Hilbert 流体系での証明を具体的に作れることがわかる。

も証明可能でなく、ゆえに → A を (よって A を) 偽とするクリプキ · モデルが作れる。

おわりに

5

以上からは、KD45 についても、シーケントを (あるいは論理式を) 与えて、それが証明可能ならその証明を実際に与え、さもなければ証明可能でないと答えるアルゴリ

シーケント計算での証明から Hilbert 流の演繹への変ズムが存在することがわかる。

換によって、命題非様相論理や命題様相論理 K, KD45 のHilbert 流の演繹体系の完全性が示せること、および同体系での証明を作り出すアルゴリズムが構成できることを

4.3 体系 KD45 での Hilbert 流の演繹体系の完全性述べた。同様の手法は、シーケント計算による演繹体系を持つものなら、他の論理体系にも応用できると考えられる。

今度も、Hilbert 流の公理のうち適当に選んだ 1 つを Tとする。正規演繹の定義も 3.3 節と同じである。
定理 4.3 任意の証明可能なシーケント S に対し、S の参考文献

Hilbert 流正規演繹が存在する。
証明 定理 3.2 とほぼ同じ。特に、[1] 萩谷昌己, 西崎真也. 論理と計算のしくみ. 岩波書店,
2007.

• Nec45 の前提に Hilbert 流正規演繹が存在する(□ A1 , · · · , □ Am , A1 , · · · , Am , ¬ □ B1 , · · · , ¬ □ Bn ,¬ □ B, ¬B ⊢◦ ¬T ) 場合、演繹定理と PD2 から⊢◦ □ A1 ⊃ · · · ⊃ □ Am ⊃ A1 ⊃ · · · ⊃ Am ⊃¬ □ B1 ⊃ · · · ⊃ ¬ □ Bn ⊃ ¬ □ B ⊃ B となり、Nec[2] 加藤暢, 高田司郎, 新出尚之. 数理論理学—合理的エー
ジェントへの応用に向けて—. コロナ社, 2014.

◦より ⊢ □(□ A1 ⊃ · · · ⊃ □ Am ⊃ A1 ⊃ · · · ⊃ Am ⊃¬ □ B1 ⊃ · · · ⊃ ¬ □ Bn ⊃ ¬ □ B ⊃ B) を得る。
公理 K と MP の適用を繰り返して □ □ A1 , · · · ,□ □ Am , □ A1 , · · · , □ Am , □ ¬ □ B1 , · · · , □ ¬ □ Bn ,◦□ ¬ □ B ⊢ □ B となるので、公理 4 と 5 および IN よ り □ A1 , · · · , □ Am , ¬ □ B1 , · · · , ¬ □ Bn ,

A

付録

A.1

Hilbert 流の体系での証明作成プログラム

本稿では、K あるいは KD45 の Hilbert 流の演繹体系に¬ □ B ⊢◦ ¬T となり、Nec45 の結論にも Hilbert 流

対し、論理式を与えてその証明を作り出すアルゴリズム

正規演繹が存在する。

の存在についても述べた。

• NecD45 の前提に Hilbert 流正規演繹が存在する

実際にそのアルゴリズムを Prolog で実装したプログラ◦(□ A1 , · · · , □ Am , A1 , · · · , Am ⊢ ¬T ) 場合、演繹定◦理から ⊢ □ A1 ⊃ · · · ⊃ □ Am ⊃ A1 ⊃ · · · ⊃ Am ⊃ム (SWI-Prolog で動作する) のファイルが、本 PDF ファイ
ルに添付されており、Adobe Reader のような添付ファイ¬T となり、Nec より ⊢◦ □(□ A1 ⊃ · · · ⊃ □ Am ⊃A1 ⊃ · · · ⊃ Am ⊃ ¬T ) を得る。
公理 K と MP の適用を繰り返して □ □ A1 , · · · ,ルを閲覧する機能を持った PDF リーダを用いれば取り出すことができるほか、UNIX 系 OS の場合は PDFtk というソフトウェアをインストールすれば、以下の手順で取◦□ □ Am , □ A1 , · · · , □ Am ⊢ □ ¬T となり、公理 4◦より □ A1 , · · · , □ Am ⊢ □ ¬T を得る。一方、Nec

り出すこともできる。

$ pdftk このPDFファイル unpack_files ◦と D から ⊢ ¬ □ ¬T なので、IN より □ A1 , · · · ,◦□ Am ⊢ ¬T となり、NecD45 の結論にも Hilbert
流正規演繹が存在する。

なお、取り出されるファイル名は hilbert.pl となっている。
既存の hilbert.pl というファイルがある場合、誤って上書

系 4.4 KD45 の Hilbert 流の演繹体系は健全かつ完全。

きしないよう注意されたい。

7

追記

これは Ax3’ と MP からすぐ出る。そこで、T を任意に選

このプログラムの以前の版では、様相オペレータ□ を、空リストと同じ記号 [] で表現していた。しかし、SWI-Prolog のバージョン 6 以降では、空リストの記号 []を op 述語でオペレータとして用いることができなくなっんだ公理とすると¬A¬A ¬A ⊃ B
MP
B
¬T

たため、本プログラムは正常に動作しなくなっていた。
本プログラムの現在の版は、様相オペレータ □ を # で
表現 (これなら何とか四角形に見える) するよう改められ¬A ⊃ ¬B
MP¬B
Weak¬¬T ⊃ ¬BCT
B ⊃ ¬TMP

より ¬A ⊃ ¬B, ¬A ⊃ B, ¬A ⊢ ¬T であり、演繹定理かたため、この問題は起きなくなっている。

ら ¬A ⊃ ¬B, ¬A ⊃ B ⊢ ¬A ⊃ ¬T となる。T が公理であることから CT, MP により ¬A ⊃ ¬B, ¬A ⊃ B ⊢ A と

A.2 ∧, ∨ を略記としない場合の演繹体系なり、再び演繹定理によって Ax3 が出る。
一方、本稿本文 (2.1 節) の体系で Ax3’ が定理であるこ∧ や ∨ を略記とせず、正式な論理オペレータとする場
合、命題 (非様相) 論理の Hilbert 流の健全かつ完全な演繹
体系は、2.1 節で示したものに、以下の公理を加えれば得とは (完全性からも従うが)、2.4.1 節の PD2 から演繹定理られる。

れを公理として採用してもよい。

で直ちにわかる。このようなわけで、Ax3 と Ax3’ はいず

Ax4 : A ∧ B ⊃ A
Ax5 : A ∧ B ⊃ B
Ax6 : A ⊃ (B ⊃ A ∧ B)
Ax7 : A ⊃ A ∨ B
Ax8 : B ⊃ A ∨ B
Ax9 : (A ⊃ C) ⊃ ((B ⊃ C) ⊃ (A ∨ B ⊃ C))
また、これらの公理を 3.1 節や 4.1 節で示した体系に追加すれば、命題様相論理 K や KD45 の Hilbert 流の健全か
つ完全な演繹体系も得られる。健全性や完全性の証明も、本稿本文と同様に可能である。

A.3 公理の別な選び方
文献によっては、2.1.1 節の公理のうち公理 Ax3 を省いて、代わりに以下の公理を置いているものもある。

Ax3’ : (¬A ⊃ ¬B) ⊃ (B ⊃ A)
このように変更した演繹体系でも、健全性・完全性はともに成り立つ。
完全性が成り立つことを示すには、この (変更後の) 体系で Ax3 が定理であることを示せば十分である。まず、Weak と演繹定理はその証明に Ax3 を用いていないため、この体系でも使えることに注意。また、以下の補助規則が使える。

¬A ⊃ ¬B
CT
B⊃A
8