1 構文的無矛盾性
本記事が扱う構文的無矛盾性は、「一階論理の証明体系」が前提集合について定めたものと同じ性質である。同記事の§E16.10 定義 7.1により、L理論S⊆Sent(L)がLにおいて構文的に無矛盾であるとは、S⊢LχかつS⊢L¬χを満たすχ∈Form(L)が存在しないことをいう。Sent(L)⊆Form(L)であるから、理論はこの定義の適用対象に含まれる。同じ記事の§E16.10 命題 7.2により、この条件は、固定した矛盾文⊥についてS⊬L⊥が成り立つことと同値である。
本記事では言語を拡大しながら理論を拡大するので、拡大した言語について無矛盾性を述べる箇所では、どの言語の導出関係について述べているかを明示する。文脈から定まる箇所では、添字を省いてS⊢χと書く。
補題 1.1.(I,⪯)を空でない全順序集合とし、各i∈Iについて、集合サイズの一階言語Liと理論Si⊆Sent(Li)が与えられているとする。さらに、i⪯jならばLi⊆LjかつSi⊆Sjが成り立ち、各SiがLiにおいて構文的に無矛盾であるとする。このとき
L∞=i∈I⋃Li,S∞=i∈I⋃Siとおくと、S∞はL∞において構文的に無矛盾である。
とくに、すべてのi∈IについてLiが同一の言語Lである場合、本補題は、包含関係で全順序付けられた無矛盾なL理論の族の合併がLにおいて無矛盾であることを与える。
証明では、導出が有限列であることを二つの目的に用いる。導出が用いる前提が有限個であることに加えて、導出に現れる非論理記号も有限個であることを用いる。前提が有限個であることだけでは、L∞における導出が、選んだ段の言語に属さない定数を用いる場合を排除することができない。
証明.S∞がL∞において矛盾すると仮定する。すなわち、S∞⊢L∞χかつS∞⊢L∞¬χを満たすχ∈Form(L∞)が存在する。この二つの§E16.10 定義 1.2の意味の導出を一つずつ固定する。
導出はいずれも有限列であり、各行の論理式は有限個の記号からなる。したがって、二つの導出の全体に現れるL∞の非論理記号は有限個であり、前提として用いるS∞の文も有限個である。記号も前提も一つも現れない場合には、Iが空でないことからi0∈Iを一つ取る。一つ以上ある場合には、現れる各記号についてその記号を含むLiの添字を、用いる各前提についてその文を含むSiの添字を、それぞれ一つずつ選ぶ。選ぶ対象が有限個なので、この選択は ZF のもとで行うことができ、選択原理を必要としない。得られた添字はIの有限部分集合であるから、⪯に関する最大元i0が存在する。単調性により、Li0は二つの導出に現れるすべての非論理記号を含み、Si0は用いたすべての前提を含む。
二つの導出に現れる論理式は、Li0の非論理記号と論理記号だけからなるので、いずれもForm(Li0)に属する。§E16.10 定義 1.2の四条件は、公理スキーマの置換例であること、先行行への modus ponens、および一般化の変数条件だけを要求し、これらはどの行の論理式もForm(Li0)に属するかぎりLi0についてそのまま成り立つ。したがって同じ二つの有限列はSi0からのLi0導出であり、Si0⊢Li0χかつSi0⊢Li0¬χである。これはSi0がLi0において構文的に無矛盾であることに反する。▨
2 有限列と構文対象の濃度
A<ω=⋃n<ωAnと書く。A0は空列だけからなる一元集合である。
補題 2.1.κを整列可能な無限濃度とする。集合Aが∣A∣≤κを満たすなら、
∣A<ω∣≤κである。特にκ<ω=κである。
集合サイズの有限項言語Lと可算無限変数集合Varについて
μ=max(ℵ0,∣L∣,∣Var∣)とおけば、
∣TermL(Var)∣≤μ,∣FormL(Var)∣≤μ,∣Sent(L)∣≤max(ℵ0,∣L∣)が成り立つ。
証明の方針は、「基数算術」が与える固定した全単射κ×κ→κを用いて、各有限冪からκへの写像を有限再帰によって一斉に定めることである。列の長さを表すタグはω×κにまとめる。一般の無限基数積は引用先が証明しているので、本記事では再証明しない。
証明.§E1.21 定理 2.2により、ZFC のもとでは任意の集合と等濃な基数がただ一つ存在する。§E1.22 定理 3.2と§E1.22 系 3.3により、無限基数κについて
∣κ×κ∣=κ,∣ω×κ∣=κである。第一の等式を与える全単射p:κ×κ→κを一つ固定する。e1:κ→κを恒等写像とし、全単射en:κn→κが定まったとき、
en+1(s,a)=p(en(s),a)と定める。有限再帰により、すべての正の整数nについて全単射enが定まる。この族は固定したpから再帰的に一意に定まるので、各nについて写像を別々に選ぶための可算選択公理を必要としない。
κは無限であるから0∈κである。空列を(0,0)へ送り、長さn>0の列sを(n,en(s))へ送ると、κ<ωからω×κへの単射を得る。§E1.22 系 3.3により、この終域の濃度はκである。逆に長さ一の列がκ個あるため、κ<ω=κである。Aからκへの単射を有限列へ成分ごとに適用すれば、∣A<ω∣≤κが従う。
構文対象の評価へ移る。変数、非論理記号、論理記号、括弧、および構文木の節を示す有限個のタグを合わせた集合をBとする。∣B∣≤μである。各項と論理式の有限構文木を、最外構成子を先に記録する前置記法の有限列へ符号化する。各記号の項数が有限であり、記号そのものが項数の情報をもつため、この符号化は単射とすることができる。したがって項集合と論理式集合はともにB<ωへ単射し、濃度は高々μである。変数集合は可算無限なので∣Var∣=ℵ0であり、μ=max(ℵ0,∣L∣)である。文集合は論理式集合の部分集合であるから、その濃度も高々max(ℵ0,∣L∣)である。▨
系 2.2.T⊆Sent(L)とし、
κ=max(ℵ0,∣L∣,∣T∣)とおく。高々κ個の定数記号を各段階で加える可算段階の Henkin 構成では、次が成り立つ。
- 各段階の言語、項集合、論理式集合、および新定数集合の濃度は高々κである。
- すべての段階の合併言語LHは∣LH∣≤κを満たす。
- LHの閉項集合と、その任意の商集合の濃度は高々κである。
- λ≥max(ℵ0,∣L∣)が無限濃度であり、λ個の新定数を加えるなら、拡大言語の濃度はちょうどλである。
証明.∣L∣≤κである。ある段階の言語の記号が高々κ個であると仮定すると、補題 2.1により、その言語の項と論理式は高々κ個である。したがって、論理式へ一つずつ新定数を割り当てても新定数は高々κ個である。既存の記号と新定数との直和はκ×2へ単射し、§E1.22 系 3.3により∣κ×2∣=κであるから、新言語の記号も高々κ個である。通常の帰納法により、各段階の言語、項集合、論理式集合、および新定数集合は高々κ個である。可算個の段階の合併はω×κへ単射し、§E1.22 系 3.3により∣ω×κ∣=κであるから、その濃度は高々κである。補題 2.1をLHへ適用すると、LHの全項集合は高々κ個である。閉項集合は全項集合の部分集合であり、商写像は閉項集合から商集合への全射なので、商の濃度も高々κである。
λ個の相異なる新定数を加えた言語は、新定数集合を部分集合として含むため濃度が少なくともλである。一方、λ≥max(ℵ0,∣L∣)である。∣L∣=0なら元の記号を加えても濃度はλのままであり、∣L∣>0なら§E1.22 系 3.3により、元の記号集合と新定数集合の和は∣L∣+λ=λである。いずれの場合も濃度は高々λである。したがって拡大言語の濃度はちょうどλである。▨
3 証人公理を一つ加える操作
まず、新しい定数を含む導出から、その定数を新鮮な変数へ置き換える構文的補題を証明する。
補題 3.1.S⊆Sent(L)とし、cをLに属さない新しい定数記号とする。S⊢L∪{c}ψ(c)ならば、新鮮な変数yを選んで
S⊢L∀yψ(y)とすることができる。ここでψ(y)は、表示されたcの出現をyへ一様に置き換えた論理式である。
証明. 与えられた導出は有限列である。導出に現れる変数を避けて新鮮な変数yを選び、必要なら導出中の束縛変数をα同値な新鮮変数へ先に変更する。導出の各行でcをyへ一様に置き換える。Sの各文はcを含まないので前提の行は変わらない。論理公理、量化公理、等号公理は一様置換後も同じ公理スキーマの例であり、modus ponens は保存される。一般化された変数はyと異なるように選び直してあるため、一般化条件も保存される。したがって、置換後の有限列はS⊢Lψ(y)を与える。
Sは文だけからなるため、yはSのどの前提にも自由に現れない。一般化規則を適用してS⊢L∀yψ(y)を得る。▨
補題 3.2.S⊆Sent(L)を構文的に無矛盾とし、FV(φ)⊆{x}とする。cをLに属さない新しい定数記号とすれば、
S∪{∃xφ(x)→φ(c)}はL∪{c}の理論として構文的に無矛盾である。
証明の方針は、証人公理を加えて矛盾すると仮定し、§E16.10 定理 5.1によって証人公理の否定をSから導くことである。新定数消去により、特定のcに対する否定をすべての要素に対する否定へ変え、S自身の矛盾を得る。
証明.A=∃xφ(x)、B=φ(c)とおく。S∪{A→B}が矛盾すると仮定する。§E16.10 定理 5.1と§E16.10 補題 2.1が与える古典命題論理の派生則によりS⊢¬(A→B)である。同じ派生則により¬(A→B)からAと¬Bがそれぞれ導かれるので、
S⊢∃xφ(x),S⊢¬φ(c)を得る。
補題 3.1を第2の導出へ適用すると、S⊢∀y¬φ(y)となる。束縛変数をxへアルファ変換するとS⊢∀x¬φ(x)である。§E16.5 定義 2.3により∃xφ(x)は¬∀x¬φ(x)の略記であるから、第1の導出S⊢∃xφ(x)はS⊢¬∀x¬φ(x)にほかならない。論理式∀x¬φ(x)とその否定がともにSから導かれるので、これはSの無矛盾性に反する。したがって証人公理を加えた理論は構文的に無矛盾である。▨
この証明はモデルも完全性定理も用いていない。使用したのは有限導出、演繹定理、量化公理、および新しい記号の一様置換だけである。
例 3.3 (証人公理を一段階加える操作).Lに一項関係記号Pがあり、S=T∪{∃xP(x)}が構文的に無矛盾であるとする。Lに属さない定数記号cを取り、
S′=S∪{∃xP(x)→P(c)}とおく。補題 3.2によりS′は構文的に無矛盾である。また、S′では前提∃xP(x)と追加した証人公理に modus ponens を適用してP(c)を導く。この無矛盾性の確認にはモデルの存在を用いていない。
拡大言語L∪{c}には、例えばP(x)∧x=cのようにcを含む新しい論理式が現れる。この論理式は最初のLに属さないため、最初の段階で証人公理を割り当てることはできない。次の段階で新定数dと
∃x(P(x)∧x=c)→(P(d)∧d=c)を加える必要がある。この新しい証人公理に対しても同じ構文的補題を適用するため、可算段階の反復が必要になる。
4 すべての証人を加える
定義 4.1.L′理論SがHenkin 理論 (Henkin theory) であるとは、FV(φ)⊆{x}を満たすすべてのL′論理式φ(x)について、ある閉項tが存在して
S⊢∃xφ(x)→φ(t)となることをいう。
定理 4.2.Lを集合サイズの有限項言語とし、T⊆Sent(L)を構文的に無矛盾とする。κ=max(ℵ0,∣L∣,∣T∣)とおく。このとき、次を満たす拡大言語LHと理論Tωが存在する。
- L⊆LH、T⊆Tω⊆Sent(LH)である。
- TωはLHにおいて構文的に無矛盾な Henkin 理論である。
- ∣LH∣≤κかつ∣Tω∣≤κである。
証明.L0=L、T0=Tとする。n段階のLn,Tnが構成され、TnがLnにおいて無矛盾であると仮定する。FV(φ)⊆{x}を満たすLn論理式と変数の組(φ,x)の集合をInとする。補題 2.1によりLn論理式は高々κ個であり、変数は可算個である。Inは論理式集合と変数集合との直積の部分集合なので、§E1.22 系 3.3により∣In∣≤κである。§E1.21 定理 2.2をInへ適用し、Inと全単射で対応する基数θnと全単射qn:θn→Inを固定する。したがってθn≤κである。qn(ξ)=(φξ,xξ)と書く。添字ξ<θnをタグとして用いることで、Lnに属さず、互いに異なる新定数cn,ξを定めることができる。
§E1.17 定理 2.1を用いて、ξ≤θnに対する言語と理論の対(Ln,ξ,Tn,ξ)を次の規則で構成する。
- (Ln,0,Tn,0)=(Ln,Tn)とする。
- ξ<θnに対して、Ln,ξ+1=Ln,ξ∪{cn,ξ}とし、
Tn,ξ+1=Tn,ξ∪{∃xξφξ(xξ)→φξ(cn,ξ)}
とする。
- 0<δ≤θnが極限順序数なら、
Ln,δ=ξ<δ⋃Ln,ξ,Tn,δ=ξ<δ⋃Tn,ξ
とする。
この再帰規則は、それ以前の対から次の対をただ一つ定めるので、§E1.17 定理 2.1の仮定を満たす。さらに§E1.17 定理 1.1を適用し、各ξ≤θnについて、Tn,ξがLn,ξにおいて無矛盾であることを示す。ξ=0ではTnの無矛盾性が仮定である。後続段ξ+1では、φξはLn⊆Ln,ξの論理式であり、cn,ξはLn,ξに属さない。したがって補題 3.2により無矛盾性が保存される。非零極限段δでは、それ以前の言語と理論の対が包含関係で増大する空でない鎖をなすので、補題 1.1により、合併した理論は合併した言語において無矛盾である。これで超限帰納法の三つの場合が閉じる。
Ln+1=Ln,θn、Tn+1=Tn,θnとおく。qnはInへの全射であるから、すべてのLn一自由変数論理式に対する証人公理がTn+1に属する。また、上の超限帰納法によりTn+1はLn+1において無矛盾である。
この操作をすべての非負整数nについて反復し、
LH=n<ω⋃Ln,Tω=n<ω⋃Tnとおく。(Ln,Tn)n<ωは言語と理論がともに増大する鎖であるから、補題 1.1によりTωはLHにおいて構文的に無矛盾である。LHの任意の論理式φは有限個の記号だけを含むため、φ∈Form(Ln)を満たす非負整数nが存在する。したがって、その一自由変数論理式に対する証人公理はTn+1で追加される。ゆえにTωは Henkin 理論である。
各nについてθn≤κであるから、各段階の新定数と証人公理は高々κ個である。系 2.2により∣LH∣≤κである。TωはTと、可算個の段階で加えた高々κ個ずつの証人公理との和集合である。§E1.22 系 3.3による∣ω×κ∣=κと∣T∣≤κから両者のタグ付き和はκ×2へ単射する。再び同じ系を用いると∣κ×2∣=κであるから、∣Tω∣≤κも従う。▨
一段階だけでは、その段階で加えた定数を含む新しい論理式の証人公理が不足する。可算段階の反復は、各論理式が有限個の記号しか含まないことと組み合わせることで、この不足を解消する。
5 Lindenbaum の補題
定義 5.1.L理論Sが Lにおいて極大無矛盾 (maximally consistent theory in L) であるとは、SがLにおいて構文的に無矛盾であり、S⊊S′⊆Sent(L)を満たしLにおいて構文的に無矛盾な理論S′が存在しないことをいう。言語が文脈から定まる場合には、単に極大無矛盾であるという。
定理 5.2 (Lindenbaum の補題). 集合サイズの言語Lにおける任意の構文的に無矛盾な理論Sは、極大無矛盾なL理論へ拡大することができる。この存在証明では Zorn の補題、したがって選択公理を用いる。
証明.Lにおいて構文的に無矛盾でありSを含むL理論の全体を、包含関係で順序付ける。この順序集合はSを含むので空でない。空でない鎖については、鎖の各要素に同じ言語Lを対応させると補題 1.1の言語が一定である特別な場合にあたるので、その合併はLにおいて構文的に無矛盾である。鎖の各要素がSを含むので合併もSを含む。したがって合併はこの順序集合に属し、鎖の上界である。空の鎖についてはS自身が上界である。§E1.20 定理 2.1 (3)の Zorn の補題を適用すると極大元S∗が存在する。S∗は定義どおり極大無矛盾なL理論である。▨
補題 5.3.Sを極大無矛盾な理論とし、σ,τを文とする。このとき、次が成り立つ。
- S⊢σであることとσ∈Sであることは同値である。
- σと¬σのちょうど一方がSに属する。
- σ→τ∈Sであることと、σ∈/Sまたはτ∈Sであることは同値である。
証明.S⊢σかつσ∈/Sとする。S∪{σ}から矛盾が導かれれば、その有限導出で前提σを用いる各箇所へSからのσの導出を代入して、Sから矛盾を導くことができる。したがってS∪{σ}は無矛盾であり、極大性に反する。ゆえにσ∈Sである。逆向きは、前提は一行の導出になることから従う。
σと¬σが両方属することは無矛盾性に反する。σ∈/Sなら、極大性によりS∪{σ}は矛盾する。§E16.10 定理 5.1と§E16.10 補題 2.1が与える古典命題論理の派生則によりS⊢¬σであり、(1)から¬σ∈Sである。したがってちょうど一方が属する。
σ→τ∈Sかつσ∈Sなら、modus ponens と(1)によりτ∈Sである。したがってσ→τ∈Sならσ∈/Sまたはτ∈Sである。逆にτ∈Sなら、§E16.10 定義 1.1の論理公理スキーマ (H1) の置換例τ→(σ→τ)と modus ponens からS⊢σ→τである。σ∈/Sなら(2)から¬σ∈Sである。§E16.10 補題 2.1 (5)が与えるσ→(¬σ→⊥ρ)と⊥ρ→τを用いるとS∪{σ}⊢τであり、§E16.10 定理 5.1によりS⊢σ→τである。(1)により、どちらの場合もσ→τ∈Sとなる。▨
6 完全な Henkin 理論
定理 6.1.Lを集合サイズの有限項言語、T⊆Sent(L)を構文的に無矛盾な理論とし、κ=max(ℵ0,∣L∣,∣T∣)とおく。このとき、拡大言語LHと理論THで、次を満たすものが存在する。
- T⊆TH⊆Sent(LH)である。
- THは極大無矛盾な Henkin 理論である。
- ∣LH∣≤κ、∣Sent(LH)∣≤κ、∣TH∣≤κである。
- FV(φ)⊆{x}かつ∃xφ(x)∈THなら、ある Henkin 定数cが存在してφ(c)∈THである。
証明.定理 4.2により、無矛盾な Henkin 理論Tω⊆Sent(LH)を得る。定理 5.2をLHの中で適用し、Tωを極大無矛盾な理論THへ拡大する。証人公理はすでにTωに属するので、THにも属する。したがってTHは Henkin 理論である。
∃xφ(x)∈THとする。対応する証人公理∃xφ(x)→φ(c)もTHに属する。
modus ponens と補題 5.3の導出閉包によりφ(c)∈THである。濃度評価は系 2.2と補題 2.1から従う。▨
7 選択公理を用いた箇所
本記事では、選択公理を次の三箇所で用いた。
- §E1.21 定理 2.2を用いて、任意の記号集合、構文対象の集合、および理論に対し、それらと等濃な基数を取った。
- 定理 4.2で、各段階の一自由変数論理式の集合を§E1.21 定理 2.2が与える基数で添字付けした。
- 定理 5.2で、「選択公理と Zorn の補題」の§E1.20 定理 2.1が与える
Zorn の補題を適用した。
§E1.22 定理 3.2と§E1.22 系 3.3の証明自体は選択公理を用いない。本記事がこれらを任意の集合の濃度へ適用するときに必要な選択公理は、第1項の基数の取り出しに含まれる。また、補題 2.1では、固定した全単射κ×κ→κから有限再帰で全写像を定めるため、可算個の写像を選ぶ選択公理は用いない。
可算言語では文を明示的な列へ並べる証明も可能である。しかし、本記事の定理は可算言語を仮定しないため、可算列挙を一般の場合の証明として用いていない。
8 演習
問題 8.1.
- 無矛盾な理論の増大列の合併が無矛盾である証明で、導出が有限であることをどこで用いるか説明せよ。
- Henkin 証人を加える操作を一段階で終えることができない理由を説明せよ。
- 補題 3.2の証明が完全性定理を用いていないことを、使用した結果の一覧から確認せよ。
- κを無限濃度とし、§E1.22 定理 3.2が与える全単射p:κ×κ→κを一つ固定する。pから有限再帰でκ<ωをω×κへ単射し、§E1.22 系 3.3を用いて∣κ<ω∣=κを証明せよ。この構成が可算選択公理を必要としない理由も述べよ。
解答 (確認問題の解答).
- 合併から矛盾を導く二つの導出について、用いる前提が有限個であることと、現れる非論理記号が有限個であることの双方に用いる。前者により、用いたすべての前提を含む段階が存在する。後者により、その段階の言語が二つの導出に現れるすべての記号を含むようにすることができる。導出が無限列であれば、前提も記号も有限個であるとはかぎらず、一つの段階を選ぶ推論は成立しない。
- 一段階で加えた新定数を含む論理式は、段階の開始時の言語には属していない。その論理式に対する証人定数は次の段階で必要になる。各論理式は有限個の記号しか含まないため、可算段階のどこかで必ず処理される。
- 使用した結果は、§E16.10 定理 5.1、§E16.10 補題 2.1が与える古典命題論理の派生則、§E16.5 定義 2.3による存在量化子の略記の展開、および補題 3.1である。モデル存在定理と完全性定理は使用していない。
- e1をκの恒等写像とし、en+1(s,a)=p(en(s),a)と定めると、有限帰納法によりen:κn→κはすべての正の整数nについて全単射である。空列を(0,0)へ送り、長さn>0の列sを(n,en(s))へ送れば、長さのタグが異なる列を分離する単射κ<ω→ω×κを得る。§E1.22 系 3.3により∣ω×κ∣=κであり、逆向きにはαを長さ一の列(α)へ送る単射があるので、§E1.21 命題 2.5と順序数の大小の反対称性により∣κ<ω∣=κである。各enは一つのpから有限再帰で一意に定まるので、可算個の写像から一つずつ選ぶ操作はない。
▨