含意命題計算

数理論理学において、含意命題計算（がんいめいだいけいさん、テンプレート:Lang-en-short）とは、含意あるいは条件法と呼ばれる一つの結合子のみを用いる古典命題計算の一形態である。論理式においては、この二項演算は「ならば」、「もし……ならば、……」、「→」、「 $\to$ 」などによって表される。

関数的（不）完全性

含意のみでは、論理演算子としては関数完全ではない。なぜなら、それだけからは他のすべての二値真理関数を構成することができないからである。

例えば、常に偽を返す二項真理関数は、→ と任意の命題変数からは定義できない。→ と命題変数から構成される論理式は、そのすべての変数が真と評価されたときに真という値を受け取らなければならないからである。したがって、{→} は関数完全ではない。

しかし、偽であることを表す0項結合子 ⊥ を加えれば、他のすべての真理関数を定義することができる。結合子の集合 {→, ⊥} 上の論理式はf-含意的と呼ばれる^[1]。P と Q を命題とすると、

¬P は P → ⊥ と同値である
P ∧ Q は (P → (Q → ⊥)) → ⊥ と同値である
P ∨ Q は (P → Q) → Q と同値である
P ↔ Q は ((P → Q) → ((Q → P) → ⊥)) → ⊥ と同値である

上記の演算子は関数完全であることが知られているので、任意の真理関数は → と ⊥ によって表現できることになる。

公理系

以下の言明は（定義により、既約かつ直観的に真であるものとして）トートロジーとみなされる。

公理図式1は P → (Q → P) である。
公理図式2は (P → (Q → R)) → ((P → Q) → (P → R)) である。
公理図式3（パースの法則）は ((P → Q) → P) → P である。
唯一の非0項推論規則（モーダスポネンス）は、P と P → Q から Q を推論するというものである。

それぞれの場合において、P、Q、R は「→」のみを結合子として含む任意の論理式に置き換えることができる。 $Γ$ を論理式の集合、A を論理式とするとき、 $Γ ⊢ A$ とは、上記の公理と規則、および $Γ$ からの論理式を追加の仮説として用いて A が導出可能であることを意味する。

ウカシェヴィッチ（1948年）は、上記の図式1〜3を単一の図式

((P → Q) → R) → ((R → P) → (S → P))

に置き換えた、含意計算のための公理系を発見した。彼はまた、これより短い公理系は存在しないと論じた^[2]。

導出の基本的性質

計算のすべての公理と規則は図式であるため、導出は代入について閉じている。

もし

Γ ⊢ A,

ならば

σ (Γ) ⊢ σ (A),

ここで σ は（含意のみを用いる論理式についての）任意の代入である。

含意命題計算はまた、演繹定理も満たす。

もし

Γ, A ⊢ B

ならば

Γ ⊢ A \to B .

演繹定理の記事で説明されているように、これは上記の公理図式1、2とモーダスポネンスを含む体系の任意の公理的拡張について成り立つ。

完全性

含意命題計算は、古典命題論理の通常の二値意味論に関して意味論的に完全である。すなわち、Γ が含意論理式の集合であり、A が Γ によって含意される含意論理式であるならば、 $Γ ⊢ A$ である。

証明

完全性定理の証明の概略を以下に示す。まず、コンパクト性定理と演繹定理を用いることで、完全性定理を Γ が空である特殊な場合に帰着させることができる。すなわち、すべてのトートロジーがこの体系において導出可能であることを示せばよい。

この証明は完全な命題論理の完全性の証明と類似しているが、含意の関数的不完全性を克服するために次のような考え方も用いる。A と F が論理式であるとき、テンプレート:Math はテンプレート:Math と同値である。ここで A* とは、A に現れる F の出現のすべて、いくつか、あるいは一つもない出現を偽で置き換えた結果である。同様に、テンプレート:Math はテンプレート:Math と同値である。したがって、ある条件下では、これらを「A* は偽である」あるいは「A* は真である」と言うことの代わりとして用いることができる。

まず、導出可能性についていくつかの基本的な事実を確認する。テンプレート:NumBlk

実際、公理1を用いて A → (B → C) を導出でき、次に公理2からモーダスポネンス（2回）によって A → C を導出できる。

テンプレート:NumBlk

これは（テンプレート:EquationNote）から演繹定理によって従う。

テンプレート:NumBlk

さらに C → B を仮定すれば、（テンプレート:EquationNote）を用いてテンプレート:Math を導出でき、次にモーダスポネンスによって C を導出できる。これにより

A \to C, (A \to B) \to C, C \to B ⊢ C

が示され、演繹定理から

A \to C, (A \to B) \to C ⊢ (C \to B) \to C

が得られる。公理3を適用すれば（テンプレート:EquationNote）が得られる。

F を任意の固定された論理式とする。任意の論理式 A に対して、テンプレート:Math およびテンプレート:Math と定義する。命題変数 p₁, ..., p_n のみからなる論理式のみを考える。これらの変数からなる任意の論理式 A と任意の真理値割り当て e について、テンプレート:NumBlk であることを主張する。（テンプレート:EquationNote）を A についての帰納法により証明する。基底段階 A = p_i は自明である。テンプレート:Math とする。三つの場合に分ける。

e(C) = 1 のとき。このとき e(A) = 1 でもある。
$(C \to F) \to F ⊢ ((B \to C) \to F) \to F$

が、公理テンプレート:Math に（テンプレート:EquationNote）を2回適用することで得られる。帰納法の仮定によりテンプレート:Math が導出されているので、テンプレート:Math を推論できる。
e(B) = 0 のとき。このときもまた e(A) = 1 である。（テンプレート:EquationNote）に演繹定理を適用すると
$B \to F ⊢ ((B \to C) \to F) \to F .$

が得られる。帰納法の仮定によりテンプレート:Math が導出されているので、テンプレート:Math を推論できる。
e(B) = 1 かつ e(C) = 0 のとき。このとき e(A) = 0 である。
$\begin{matrix} (B \to F) \to F, C \to F, B \to C & ⊢ B \to F & (1)により \\ ⊢ F & モーダスポネンスにより, \end{matrix}$

したがって、演繹定理により $(B \to F) \to F, C \to F ⊢ (B \to C) \to F$ が得られる。帰納法の仮定によりテンプレート:Math とテンプレート:Math を導出しているので、テンプレート:Math を推論できる。これで（テンプレート:EquationNote）の証明が完了する。

次に、F を変数 p₁, ..., p_n におけるトートロジーとする。任意の割り当て e について、k = n,...,0 に関する逆向きの帰納法により、テンプレート:NumBlk を証明する。基底段階 k = n は、

F^{e (F)} = F^{1} = ((F \to F) \to F)

を用いた（テンプレート:EquationNote）の特殊な場合と、演繹定理により F→F が定理であるという事実から従う。

（テンプレート:EquationNote）が k + 1 について成り立つと仮定し、k についてそれを示す。演繹定理を帰納法の仮定に適用すると、e(p_k+1) = 0 とした場合と e(p_k+1) = 1 とした場合とで、それぞれ

\begin{matrix} p_{1}^{e (p_{1})}, \dots, p_{k}^{e (p_{k})} & ⊢ (p_{k + 1} \to F) \to F, \\ p_{1}^{e (p_{1})}, \dots, p_{k}^{e (p_{k})} & ⊢ ((p_{k + 1} \to F) \to F) \to F, \end{matrix}

が得られる。これらから、モーダスポネンスを用いて（テンプレート:EquationNote）を導出する。

k = 0 のとき、トートロジー F が仮定なしに証明可能であることが得られる。これが証明すべきことであった。

この証明は構成的である。つまり、あるトートロジーが与えられれば、実際にこの手順に従って公理からその証明を作成することができる。しかし、そのような証明の長さは、トートロジーに含まれる命題変数の数に対して指数関数的に増加するため、非常に短いトートロジーを除けば実用的な方法ではない。

ベルナイス＝タルスキーの公理系

ベルナイス＝タルスキーの公理系はしばしば用いられる。特に、ウカシェヴィッチの論文は、その完全性を示す手段として、ウカシェヴィッチの単一公理からベルナイス＝タルスキーの公理を導出している。
この公理系は、上記の公理図式2、(P→(Q→R))→((P→Q)→(P→R))、を

公理図式2': (P→Q)→((Q→R)→(P→R))

に置き換える点で異なっており、これは仮言三段論法と呼ばれる。これにより演繹メタ定理の導出はいくぶん難しくなるが、それでも行うことができる。

P→(Q→R) と P→Q から P→R を導出できることを示す。この事実は、メタ定理を得るために公理図式2の代わりに用いることができる。

P→(Q→R) 前提
P→Q 前提
(P→Q)→((Q→R)→(P→R)) 公理2'
(Q→R)→(P→R) mp 2,3
(P→(Q→R))→(((Q→R)→(P→R))→(P→(P→R))) 公理2'
((Q→R)→(P→R))→(P→(P→R)) mp 1,5
P→(P→R) mp 4,6
(P→(P→R))→(((P→R)→R)→(P→R)) 公理2'
((P→R)→R)→(P→R) mp 7,8
(((P→R)→R)→(P→R))→(P→R) 公理3
P→R mp 9,10 証明終

充足可能性と妥当性

テンプレート:Main

含意命題計算における充足可能性は自明である。なぜなら、すべての論理式は充足可能だからである。すべての変数を真とすればよい。

含意命題計算における反証可能性はNP完全である^[3]。これは、妥当性（トートロジー性）がco-NP完全であることを意味する。

この場合、有用な手法は、その論理式がトートロジーではないと仮定し、それを偽にする付値を見つけようとすることである。もし成功すれば、それは実際にトートロジーではない。もし失敗すれば、それはトートロジーである。

非トートロジーの例：

[(A→B)→((C→A)→E)]→([F→((C→D)→E)]→[(A→F)→(D→E)]) が偽であると仮定する。

このとき (A→B)→((C→A)→E) は真であり、F→((C→D)→E) は真であり、A→F は真であり、D は真であり、E は偽である。

D が真なので、C→D は真である。したがって F→((C→D)→E) の真理値は F→E の真理値と等価である。

すると E が偽で F→E が真であることから、F は偽であることが得られる。

A→F が真なので、A は偽である。したがって A→B は真であり、(C→A)→E は真である。

C→A は偽であるから、C は真である。

B の値は結果に影響しないので、任意に真を選ぶことができる。

まとめると、B、C、D を真とし、A、E、F を偽とする付値により、[(A→B)→((C→A)→E)]→([F→((C→D)→E)]→[(A→F)→(D→E)]) は偽になる。したがってこれはトートロジーではない。

トートロジーの例：

((A→B)→C)→((C→A)→(D→A)) が偽であると仮定する。

このとき (A→B)→C は真であり、C→A は真であり、D は真であり、A は偽である。

A が偽なので、A→B は真である。したがって C は真である。したがって A は真でなければならず、これは A が偽であるという事実と矛盾する。

したがって、((A→B)→C)→((C→A)→(D→A)) を偽にする付値は存在しない。よって、これはトートロジーである。

公理図式の追加

上記に挙げたものに別の公理図式を追加した場合、何が起こるだろうか。二つの場合がある。（1）それがトートロジーである場合、または（2）それがトートロジーでない場合である。

それがトートロジーである場合、定理の集合は以前と同様にトートロジーの集合のままである。しかし、場合によっては定理のかなり短い証明を見つけられることがある。それでもなお、定理の証明の最小長は無制限のままである。すなわち、任意の自然数 n に対して、n 以下のステップでは証明できない定理が依然として存在する。

新しい公理図式がトートロジーでない場合、すべての論理式が定理になってしまう（これはこの場合、定理という概念を無意味にしてしまう）。さらに、すべての論理式を証明するための共通の方法が存在するため、すべての論理式の証明の最小長には上界が存在することになる。例えば、新しい公理図式が ((B→C)→C)→B であるとする。このとき ((A→(A→A))→(A→A))→A はその一つの事例（新しい公理の一つ）であり、これもトートロジーではない。しかし [((A→(A→A))→(A→A))→A]→A はトートロジーであり、したがって（上記の完全性の結果を用いれば）古い公理による定理である。モーダスポネンスを適用すると、A は拡張された体系の定理であることがわかる。このとき、任意の論理式を証明するために必要なことは、A の証明全体において A を望みの論理式に置き換えることだけである。この証明は A の証明と同じ数のステップを持つことになる。

別の公理化

上記に挙げた公理は、主として演繹メタ定理を通じて完全性に到達する。ここでは、演繹メタ定理を経由せずに直接完全性を目指す別の公理系を示す。

まず、ただ一つの命題変数のみを含むトートロジーの部分集合を効率的に証明するように設計された公理図式がある。

aa 1: ꞈA→A
aa 2: (A→B)→ꞈ(A→(C→B))
aa 3: A→((B→C)→ꞈ((A→B)→C))
aa 4: A→ꞈ(B→A)

このようなトートロジーの証明は、いずれも同一である二つの部分（仮説と結論）から始まる。次に、その間に追加の仮説を挿入する。次に、（唯一の変数が偽であっても真であるような）追加のトートロジー的仮説を元の仮説の中に挿入する。次に、外側（左側）にさらに仮説を追加する。この手続きにより、ただ一つの変数のみを含むすべてのトートロジーが速やかに得られる。（各公理図式中の記号「ꞈ」は、完全性の証明で用いられる結論がどこから始まるかを示している。これは単なる注釈であり、論理式の一部ではない。）

A、B、C₁, ..., C_n を含みうり、最終的な結論としてA で終わる任意の論理式 Φ を考える。このとき、

aa 5: Φ₋→(Φ₊→ꞈΦ)

を公理図式として採る。ここで Φ₋ は Φ 全体において B を A で置き換えた結果であり、Φ₊ は Φ 全体において B を (A→A) で置き換えた結果である。ここには二段階の代入があるため、これは公理図式のための図式である。すなわち、第一段階では Φ が（変化を伴いつつ）代入され、第二段階では、（A と B の両方を含む）任意の変数が含意命題計算の任意の論理式に置き換えられうる。この図式により、B が偽である場合 Φ₋ と、B が真である場合 Φ₊ とを考えることで、一つ以上の変数を含むトートロジーを証明できるようになる。

ある論理式の最終的な結論である変数が真の値をとるならば、他の変数の値にかかわらず、論理式全体は真の値をとる。したがって A が真であれば、Φ、Φ₋、Φ₊、および Φ₋→(Φ₊→Φ) はすべて真である。したがって一般性を失うことなく、A は偽であると仮定してよい。Φ がトートロジーであることと、Φ₋ と Φ₊ の両方がトートロジーであることとは同値であることに注意されたい。しかし Φ が n+2 個の異なる変数を持つのに対し、Φ₋ と Φ₊ はいずれも n+1 個しか持たない。したがって、ある論理式がトートロジーであるかという問いは、それぞれ一つの変数のみを含むある論理式がすべてトートロジーであるかという問いに帰着される。また、Φ₋→(Φ₊→Φ) は、Φ がトートロジーであるかどうかにかかわらずトートロジーであることにも注意されたい。なぜなら、Φ が偽であれば、B が偽であるか真であるかに応じて、Φ₋ か Φ₊ のいずれかが偽になるからである。

例：

パースの法則の導出

[((P→P)→P)→P]→([((P→(P→P))→P)→P]→[((P→Q)→P)→P]) aa 5
P→P aa 1
(P→P)→((P→P)→(((P→P)→P)→P)) aa 3
(P→P)→(((P→P)→P)→P) mp 2,3
((P→P)→P)→P mp 2,4
[((P→(P→P))→P)→P]→[((P→Q)→P)→P] mp 5,1
P→(P→P) aa 4
(P→(P→P))→((P→P)→(((P→(P→P))→P)→P)) aa 3
(P→P)→(((P→(P→P))→P)→P) mp 7,8
((P→(P→P))→P)→P mp 2,9
((P→Q)→P)→P mp 10,6 証明終

ウカシェヴィッチの単一公理の導出

[((P→Q)→P)→((P→P)→(S→P))]→([((P→Q)→(P→P))→(((P→P)→P)→(S→P))]→[((P→Q)→R)→((R→P)→(S→P))]) aa 5
[((P→P)→P)→((P→P)→(S→P))]→([((P→(P→P))→P)→((P→P)→(S→P))]→[((P→Q)→P)→((P→P)→(S→P))]) aa 5
P→(S→P) aa 4
(P→(S→P))→(P→((P→P)→(S→P))) aa 2
P→((P→P)→(S→P)) mp 3,4
P→P aa 1
(P→P)→((P→((P→P)→(S→P)))→[((P→P)→P)→((P→P)→(S→P))]) aa 3
(P→((P→P)→(S→P)))→[((P→P)→P)→((P→P)→(S→P))] mp 6,7
((P→P)→P)→((P→P)→(S→P)) mp 5,8
[((P→(P→P))→P)→((P→P)→(S→P))]→[((P→Q)→P)→((P→P)→(S→P))] mp 9,2
P→(P→P) aa 4
(P→(P→P))→((P→((P→P)→(S→P)))→[((P→(P→P))→P)→((P→P)→(S→P))]) aa 3
(P→((P→P)→(S→P)))→[((P→(P→P))→P)→((P→P)→(S→P))] mp 11,12
((P→(P→P))→P)→((P→P)→(S→P)) mp 5,13
((P→Q)→P)→((P→P)→(S→P)) mp 14,10
[((P→Q)→(P→P))→(((P→P)→P)→(S→P))]→[((P→Q)→R)→((R→P)→(S→P))] mp 15,1
(P→P)→((P→(S→P))→[((P→P)→P)→(S→P)]) aa 3
(P→(S→P))→[((P→P)→P)→(S→P)] mp 6,17
((P→P)→P)→(S→P) mp 3,18
(((P→P)→P)→(S→P))→[((P→Q)→(P→P))→(((P→P)→P)→(S→P))] aa 4
((P→Q)→(P→P))→(((P→P)→P)→(S→P)) mp 19,20
((P→Q)→R)→((R→P)→(S→P)) mp 21,16 証明終

ウカシェヴィッチの単一公理を真理値表によって検証するには、4個の異なる変数を含むため 16=2⁴ 通りの場合を考慮する必要がある。この導出においては、R が偽で Q が偽、R が偽で Q が真、R が真、というわずか3通りの場合のみを考慮すればよかった。しかし、私たちは論理の（形式の外にある非形式的なものとしてではなく）形式体系の内部で作業しているため、それぞれの場合はより多くの労力を要した。

出典

テンプレート:Reflist

さらなる読書

Mendelson, Elliot (1997) Introduction to Mathematical Logic, 4th ed. London: Chapman & Hall.

↑ テンプレート:Cite journal
↑ Łukasiewicz, Jan (1948) The shortest axiom of the implicational calculus of propositions, Proc. Royal Irish Academy, vol. 52, sec. A, no. 3, pp. 25–33.
↑ テンプレート:Cite journal

[1] テンプレート:Cite journal

[2] Łukasiewicz, Jan (1948) The shortest axiom of the implicational calculus of propositions, Proc. Royal Irish Academy, vol. 52, sec. A, no. 3, pp. 25–33.

[3] テンプレート:Cite journal

[1]

[2]

[3]

含意命題計算

目次

関数的（不）完全性

公理系

導出の基本的性質

完全性

証明

ベルナイス＝タルスキーの公理系

充足可能性と妥当性

公理図式の追加

別の公理化

関連項目

出典

さらなる読書

ナビゲーションメニュー

含意命題計算

関数的（不）完全性

公理系

導出の基本的性質

完全性

証明

ベルナイス＝タルスキーの公理系

充足可能性と妥当性

公理図式の追加

別の公理化

関連項目

出典

さらなる読書

ナビゲーション メニュー

検索

ナビゲーションメニュー