§E16.11無矛盾性と Henkin 拡大

最終更新

完全性定理のモデルを構成するためには、存在文が理論から導かれるたびに、その証人を名前で指すことができなければならない。 Henkin 拡大は、新しい定数cφc_\varphiと証人公理

∃xφ(x)→φ(cφ)\exists x\varphi(x)\to\varphi(c_\varphi)

を加える。証人公理を加える操作は意味論的なモデルの存在を使わず、構文的無矛盾性だけを保存しなければならない。モデルの存在を使って無矛盾性を証明すると、そのモデルを後で Henkin 拡大から構成する論証が循環するためである。

本記事では、任意の集合サイズの言語を扱う。したがって、文を可算列へ並べる方法には限定しない。「基数とアレフ」と「基数算術」が与える一般定理を構文対象の濃度評価へ適用し、「超限帰納法と超限再帰」を証人追加の構成へ適用する。極大無矛盾理論の存在には「選択公理と Zorn の補題」の Zorn の補題を用いる。

1 構文的無矛盾性

本記事が扱う構文的無矛盾性は、「一階論理の証明体系」が前提集合について定めたものと同じ性質である。同記事の§E16.10 定義 7.1により、LL理論S⊆Sent⁡(L)S\subseteq\operatorname{Sent}(L)がLLにおいて構文的に無矛盾であるとは、S⊢LχS\vdash_L\chiかつS⊢L¬χS\vdash_L\neg\chiを満たすχ∈Form⁡(L)\chi\in\operatorname{Form}(L)が存在しないことをいう。Sent⁡(L)⊆Form⁡(L)\operatorname{Sent}(L)\subseteq\operatorname{Form}(L)であるから、理論はこの定義の適用対象に含まれる。同じ記事の§E16.10 命題 7.2により、この条件は、固定した矛盾文⊥\botについてS⊬L⊥S\nvdash_L\botが成り立つことと同値である。

本記事では言語を拡大しながら理論を拡大するので、拡大した言語について無矛盾性を述べる箇所では、どの言語の導出関係について述べているかを明示する。文脈から定まる箇所では、添字を省いてS⊢χS\vdash\chiと書く。

補題 1.1.(I,⪯)(I,\preceq)を空でない全順序集合とし、各i∈Ii\in Iについて、集合サイズの一階言語LiL_iと理論Si⊆Sent⁡(Li)S_i\subseteq\operatorname{Sent}(L_i)が与えられているとする。さらに、i⪯ji\preceq jならばLi⊆LjL_i\subseteq L_jかつSi⊆SjS_i\subseteq S_jが成り立ち、各SiS_iがLiL_iにおいて構文的に無矛盾であるとする。このとき

L∞=⋃i∈ILi,S∞=⋃i∈ISiL_\infty=\bigcup_{i\in I}L_i, \qquad S_\infty=\bigcup_{i\in I}S_i

とおくと、S∞S_\inftyはL∞L_\inftyにおいて構文的に無矛盾である。

とくに、すべてのi∈Ii\in IについてLiL_iが同一の言語LLである場合、本補題は、包含関係で全順序付けられた無矛盾なLL理論の族の合併がLLにおいて無矛盾であることを与える。

証明では、導出が有限列であることを二つの目的に用いる。導出が用いる前提が有限個であることに加えて、導出に現れる非論理記号も有限個であることを用いる。前提が有限個であることだけでは、L∞L_\inftyにおける導出が、選んだ段の言語に属さない定数を用いる場合を排除することができない。

証明.S∞S_\inftyがL∞L_\inftyにおいて矛盾すると仮定する。すなわち、S∞⊢L∞χS_\infty\vdash_{L_\infty}\chiかつS∞⊢L∞¬χS_\infty\vdash_{L_\infty}\neg\chiを満たすχ∈Form⁡(L∞)\chi\in\operatorname{Form}(L_\infty)が存在する。この二つの§E16.10 定義 1.2の意味の導出を一つずつ固定する。

導出はいずれも有限列であり、各行の論理式は有限個の記号からなる。したがって、二つの導出の全体に現れるL∞L_\inftyの非論理記号は有限個であり、前提として用いるS∞S_\inftyの文も有限個である。記号も前提も一つも現れない場合には、IIが空でないことからi0∈Ii_0\in Iを一つ取る。一つ以上ある場合には、現れる各記号についてその記号を含むLiL_iの添字を、用いる各前提についてその文を含むSiS_iの添字を、それぞれ一つずつ選ぶ。選ぶ対象が有限個なので、この選択は ZF のもとで行うことができ、選択原理を必要としない。得られた添字はIIの有限部分集合であるから、⪯\preceqに関する最大元i0i_0が存在する。単調性により、Li0L_{i_0}は二つの導出に現れるすべての非論理記号を含み、Si0S_{i_0}は用いたすべての前提を含む。

二つの導出に現れる論理式は、Li0L_{i_0}の非論理記号と論理記号だけからなるので、いずれもForm⁡(Li0)\operatorname{Form}(L_{i_0})に属する。§E16.10 定義 1.2の四条件は、公理スキーマの置換例であること、先行行への modus ponens、および一般化の変数条件だけを要求し、これらはどの行の論理式もForm⁡(Li0)\operatorname{Form}(L_{i_0})に属するかぎりLi0L_{i_0}についてそのまま成り立つ。したがって同じ二つの有限列はSi0S_{i_0}からのLi0L_{i_0}導出であり、Si0⊢Li0χS_{i_0}\vdash_{L_{i_0}}\chiかつSi0⊢Li0¬χS_{i_0}\vdash_{L_{i_0}}\neg\chiである。これはSi0S_{i_0}がLi0L_{i_0}において構文的に無矛盾であることに反する。▨

2 有限列と構文対象の濃度

A<ω=⋃n<ωAnA^{<\omega}=\bigcup_{n<\omega}A^nと書く。A0A^0は空列だけからなる一元集合である。

補題 2.1.κ\kappaを整列可能な無限濃度とする。集合AAが∣A∣≤κ|A|\le\kappaを満たすなら、

∣A<ω∣≤κ|A^{<\omega}|\le\kappa

である。特にκ<ω=κ\kappa^{<\omega}=\kappaである。

集合サイズの有限項言語LLと可算無限変数集合Var\mathrm{Var}について

μ=max⁡(ℵ0,∣L∣,∣Var∣)\mu=\max(\aleph_0,|L|,|\mathrm{Var}|)

とおけば、

∣Term⁡L(Var)∣≤μ,∣Form⁡L(Var)∣≤μ,∣Sent⁡(L)∣≤max⁡(ℵ0,∣L∣)|\operatorname{Term}_L(\mathrm{Var})|\le\mu, \qquad |\operatorname{Form}_L(\mathrm{Var})|\le\mu, \qquad |\operatorname{Sent}(L)|\le\max(\aleph_0,|L|)

が成り立つ。

証明の方針は、「基数算術」が与える固定した全単射κ×κ→κ\kappa\times\kappa\to\kappaを用いて、各有限冪からκ\kappaへの写像を有限再帰によって一斉に定めることである。列の長さを表すタグはω×κ\omega\times\kappaにまとめる。一般の無限基数積は引用先が証明しているので、本記事では再証明しない。

証明.§E1.21 定理 2.2により、ZFC のもとでは任意の集合と等濃な基数がただ一つ存在する。§E1.22 定理 3.2と§E1.22 系 3.3により、無限基数κ\kappaについて

∣κ×κ∣=κ,∣ω×κ∣=κ|\kappa\times\kappa|=\kappa, \qquad |\omega\times\kappa|=\kappa

である。第一の等式を与える全単射p:κ×κ→κp:\kappa\times\kappa\to\kappaを一つ固定する。e1:κ→κe_1:\kappa\to\kappaを恒等写像とし、全単射en:κn→κe_n:\kappa^n\to\kappaが定まったとき、

en+1(s,a)=p(en(s),a)e_{n+1}(s,a)=p(e_n(s),a)

と定める。有限再帰により、すべての正の整数nnについて全単射ene_nが定まる。この族は固定したppから再帰的に一意に定まるので、各nnについて写像を別々に選ぶための可算選択公理を必要としない。

κ\kappaは無限であるから0∈κ0\in\kappaである。空列を(0,0)(0,0)へ送り、長さn>0n>0の列ssを(n,en(s))(n,e_n(s))へ送ると、κ<ω\kappa^{<\omega}からω×κ\omega\times\kappaへの単射を得る。§E1.22 系 3.3により、この終域の濃度はκ\kappaである。逆に長さ一の列がκ\kappa個あるため、κ<ω=κ\kappa^{<\omega}=\kappaである。AAからκ\kappaへの単射を有限列へ成分ごとに適用すれば、∣A<ω∣≤κ|A^{<\omega}|\le\kappaが従う。

構文対象の評価へ移る。変数、非論理記号、論理記号、括弧、および構文木の節を示す有限個のタグを合わせた集合をBBとする。∣B∣≤μ|B|\le\muである。各項と論理式の有限構文木を、最外構成子を先に記録する前置記法の有限列へ符号化する。各記号の項数が有限であり、記号そのものが項数の情報をもつため、この符号化は単射とすることができる。したがって項集合と論理式集合はともにB<ωB^{<\omega}へ単射し、濃度は高々μ\muである。変数集合は可算無限なので∣Var∣=ℵ0|\mathrm{Var}|=\aleph_0であり、μ=max⁡(ℵ0,∣L∣)\mu=\max(\aleph_0,|L|)である。文集合は論理式集合の部分集合であるから、その濃度も高々max⁡(ℵ0,∣L∣)\max(\aleph_0,|L|)である。▨

系 2.2.T⊆Sent⁡(L)T\subseteq\operatorname{Sent}(L)とし、

κ=max⁡(ℵ0,∣L∣,∣T∣)\kappa=\max(\aleph_0,|L|,|T|)

とおく。高々κ\kappa個の定数記号を各段階で加える可算段階の Henkin 構成では、次が成り立つ。

  1. 各段階の言語、項集合、論理式集合、および新定数集合の濃度は高々κ\kappaである。
  2. すべての段階の合併言語LHL^Hは∣LH∣≤κ|L^H|\le\kappaを満たす。
  3. LHL^Hの閉項集合と、その任意の商集合の濃度は高々κ\kappaである。
  4. λ≥max⁡(ℵ0,∣L∣)\lambda\ge\max(\aleph_0,|L|)が無限濃度であり、λ\lambda個の新定数を加えるなら、拡大言語の濃度はちょうどλ\lambdaである。

証明.∣L∣≤κ|L|\le\kappaである。ある段階の言語の記号が高々κ\kappa個であると仮定すると、補題 2.1により、その言語の項と論理式は高々κ\kappa個である。したがって、論理式へ一つずつ新定数を割り当てても新定数は高々κ\kappa個である。既存の記号と新定数との直和はκ×2\kappa\times 2へ単射し、§E1.22 系 3.3により∣κ×2∣=κ|\kappa\times 2|=\kappaであるから、新言語の記号も高々κ\kappa個である。通常の帰納法により、各段階の言語、項集合、論理式集合、および新定数集合は高々κ\kappa個である。可算個の段階の合併はω×κ\omega\times\kappaへ単射し、§E1.22 系 3.3により∣ω×κ∣=κ|\omega\times\kappa|=\kappaであるから、その濃度は高々κ\kappaである。補題 2.1をLHL^Hへ適用すると、LHL^Hの全項集合は高々κ\kappa個である。閉項集合は全項集合の部分集合であり、商写像は閉項集合から商集合への全射なので、商の濃度も高々κ\kappaである。

λ\lambda個の相異なる新定数を加えた言語は、新定数集合を部分集合として含むため濃度が少なくともλ\lambdaである。一方、λ≥max⁡(ℵ0,∣L∣)\lambda\ge\max(\aleph_0,|L|)である。∣L∣=0|L|=0なら元の記号を加えても濃度はλ\lambdaのままであり、∣L∣>0|L|>0なら§E1.22 系 3.3により、元の記号集合と新定数集合の和は∣L∣+λ=λ|L|+\lambda=\lambdaである。いずれの場合も濃度は高々λ\lambdaである。したがって拡大言語の濃度はちょうどλ\lambdaである。▨

3 証人公理を一つ加える操作

まず、新しい定数を含む導出から、その定数を新鮮な変数へ置き換える構文的補題を証明する。

補題 3.1.S⊆Sent⁡(L)S\subseteq\operatorname{Sent}(L)とし、ccをLLに属さない新しい定数記号とする。S⊢L∪{c}ψ(c)S\vdash_{L\cup\{c\}}\psi(c)ならば、新鮮な変数yyを選んで

S⊢L∀y ψ(y)S\vdash_L\forall y\,\psi(y)

とすることができる。ここでψ(y)\psi(y)は、表示されたccの出現をyyへ一様に置き換えた論理式である。

証明. 与えられた導出は有限列である。導出に現れる変数を避けて新鮮な変数yyを選び、必要なら導出中の束縛変数をα\alpha同値な新鮮変数へ先に変更する。導出の各行でccをyyへ一様に置き換える。SSの各文はccを含まないので前提の行は変わらない。論理公理、量化公理、等号公理は一様置換後も同じ公理スキーマの例であり、modus ponens は保存される。一般化された変数はyyと異なるように選び直してあるため、一般化条件も保存される。したがって、置換後の有限列はS⊢Lψ(y)S\vdash_L\psi(y)を与える。

SSは文だけからなるため、yyはSSのどの前提にも自由に現れない。一般化規則を適用してS⊢L∀yψ(y)S\vdash_L\forall y\psi(y)を得る。▨

補題 3.2.S⊆Sent⁡(L)S\subseteq\operatorname{Sent}(L)を構文的に無矛盾とし、FV(φ)⊆{x}FV(\varphi)\subseteq\{x\}とする。ccをLLに属さない新しい定数記号とすれば、

S∪{∃xφ(x)→φ(c)}S\cup\{\exists x\varphi(x)\to\varphi(c)\}

はL∪{c}L\cup\{c\}の理論として構文的に無矛盾である。

証明の方針は、証人公理を加えて矛盾すると仮定し、§E16.10 定理 5.1によって証人公理の否定をSSから導くことである。新定数消去により、特定のccに対する否定をすべての要素に対する否定へ変え、SS自身の矛盾を得る。

証明.A=∃xφ(x)A=\exists x\varphi(x)、B=φ(c)B=\varphi(c)とおく。S∪{A→B}S\cup\{A\to B\}が矛盾すると仮定する。§E16.10 定理 5.1と§E16.10 補題 2.1が与える古典命題論理の派生則によりS⊢¬(A→B)S\vdash\neg(A\to B)である。同じ派生則により¬(A→B)\neg(A\to B)からAAと¬B\neg Bがそれぞれ導かれるので、

S⊢∃xφ(x),S⊢¬φ(c)S\vdash\exists x\varphi(x), \qquad S\vdash\neg\varphi(c)

を得る。

補題 3.1を第2の導出へ適用すると、S⊢∀y¬φ(y)S\vdash\forall y\neg\varphi(y)となる。束縛変数をxxへアルファ変換するとS⊢∀x¬φ(x)S\vdash\forall x\neg\varphi(x)である。§E16.5 定義 2.3により∃xφ(x)\exists x\varphi(x)は¬∀x¬φ(x)\neg\forall x\neg\varphi(x)の略記であるから、第1の導出S⊢∃xφ(x)S\vdash\exists x\varphi(x)はS⊢¬∀x¬φ(x)S\vdash\neg\forall x\neg\varphi(x)にほかならない。論理式∀x¬φ(x)\forall x\neg\varphi(x)とその否定がともにSSから導かれるので、これはSSの無矛盾性に反する。したがって証人公理を加えた理論は構文的に無矛盾である。▨

この証明はモデルも完全性定理も用いていない。使用したのは有限導出、演繹定理、量化公理、および新しい記号の一様置換だけである。

例 3.3 (証人公理を一段階加える操作).LLに一項関係記号PPがあり、S=T∪{∃xP(x)}S=T\cup\{\exists xP(x)\}が構文的に無矛盾であるとする。LLに属さない定数記号ccを取り、

S′=S∪{∃xP(x)→P(c)}S'=S\cup\{\exists xP(x)\to P(c)\}

とおく。補題 3.2によりS′S'は構文的に無矛盾である。また、S′S'では前提∃xP(x)\exists xP(x)と追加した証人公理に modus ponens を適用してP(c)P(c)を導く。この無矛盾性の確認にはモデルの存在を用いていない。

拡大言語L∪{c}L\cup\{c\}には、例えばP(x)∧x≠cP(x)\land x\ne cのようにccを含む新しい論理式が現れる。この論理式は最初のLLに属さないため、最初の段階で証人公理を割り当てることはできない。次の段階で新定数ddと

∃x(P(x)∧x≠c)→(P(d)∧d≠c)\exists x\bigl(P(x)\land x\ne c\bigr)\to\bigl(P(d)\land d\ne c\bigr)

を加える必要がある。この新しい証人公理に対しても同じ構文的補題を適用するため、可算段階の反復が必要になる。

4 すべての証人を加える

定義 4.1.L′L'理論SSがHenkin 理論 (Henkin theory) であるとは、FV(φ)⊆{x}FV(\varphi)\subseteq\{x\}を満たすすべてのL′L'論理式φ(x)\varphi(x)について、ある閉項ttが存在して

S⊢∃xφ(x)→φ(t)S\vdash\exists x\varphi(x)\to\varphi(t)

となることをいう。

定理 4.2.LLを集合サイズの有限項言語とし、T⊆Sent⁡(L)T\subseteq\operatorname{Sent}(L)を構文的に無矛盾とする。κ=max⁡(ℵ0,∣L∣,∣T∣)\kappa=\max(\aleph_0,|L|,|T|)とおく。このとき、次を満たす拡大言語LHL^Hと理論TωT_\omegaが存在する。

  1. L⊆LHL\subseteq L^H、T⊆Tω⊆Sent⁡(LH)T\subseteq T_\omega\subseteq\operatorname{Sent}(L^H)である。
  2. TωT_\omegaはLHL^Hにおいて構文的に無矛盾な Henkin 理論である。
  3. ∣LH∣≤κ|L^H|\le\kappaかつ∣Tω∣≤κ|T_\omega|\le\kappaである。

証明.L0=LL_0=L、T0=TT_0=Tとする。nn段階のLn,TnL_n,T_nが構成され、TnT_nがLnL_nにおいて無矛盾であると仮定する。FV(φ)⊆{x}FV(\varphi)\subseteq\{x\}を満たすLnL_n論理式と変数の組(φ,x)(\varphi,x)の集合をInI_nとする。補題 2.1によりLnL_n論理式は高々κ\kappa個であり、変数は可算個である。InI_nは論理式集合と変数集合との直積の部分集合なので、§E1.22 系 3.3により∣In∣≤κ|I_n|\le\kappaである。§E1.21 定理 2.2をInI_nへ適用し、InI_nと全単射で対応する基数θn\theta_nと全単射qn:θn→Inq_n:\theta_n\to I_nを固定する。したがってθn≤κ\theta_n\le\kappaである。qn(ξ)=(φξ,xξ)q_n(\xi)=(\varphi_\xi,x_\xi)と書く。添字ξ<θn\xi<\theta_nをタグとして用いることで、LnL_nに属さず、互いに異なる新定数cn,ξc_{n,\xi}を定めることができる。

§E1.17 定理 2.1を用いて、ξ≤θn\xi\le\theta_nに対する言語と理論の対(Ln,ξ,Tn,ξ)(L_{n,\xi},T_{n,\xi})を次の規則で構成する。

  1. (Ln,0,Tn,0)=(Ln,Tn)(L_{n,0},T_{n,0})=(L_n,T_n)とする。
  2. ξ<θn\xi<\theta_nに対して、Ln,ξ+1=Ln,ξ∪{cn,ξ}L_{n,\xi+1}=L_{n,\xi}\cup\{c_{n,\xi}\}とし、 Tn,ξ+1=Tn,ξ∪{∃xξφξ(xξ)→φξ(cn,ξ)}T_{n,\xi+1}=T_{n,\xi}\cup \{\exists x_\xi\varphi_\xi(x_\xi)\to\varphi_\xi(c_{n,\xi})\} とする。
  3. 0<δ≤θn0<\delta\le\theta_nが極限順序数なら、 Ln,δ=⋃ξ<δLn,ξ,Tn,δ=⋃ξ<δTn,ξL_{n,\delta}=\bigcup_{\xi<\delta}L_{n,\xi}, \qquad T_{n,\delta}=\bigcup_{\xi<\delta}T_{n,\xi} とする。

この再帰規則は、それ以前の対から次の対をただ一つ定めるので、§E1.17 定理 2.1の仮定を満たす。さらに§E1.17 定理 1.1を適用し、各ξ≤θn\xi\le\theta_nについて、Tn,ξT_{n,\xi}がLn,ξL_{n,\xi}において無矛盾であることを示す。ξ=0\xi=0ではTnT_nの無矛盾性が仮定である。後続段ξ+1\xi+1では、φξ\varphi_\xiはLn⊆Ln,ξL_n\subseteq L_{n,\xi}の論理式であり、cn,ξc_{n,\xi}はLn,ξL_{n,\xi}に属さない。したがって補題 3.2により無矛盾性が保存される。非零極限段δ\deltaでは、それ以前の言語と理論の対が包含関係で増大する空でない鎖をなすので、補題 1.1により、合併した理論は合併した言語において無矛盾である。これで超限帰納法の三つの場合が閉じる。

Ln+1=Ln,θnL_{n+1}=L_{n,\theta_n}、Tn+1=Tn,θnT_{n+1}=T_{n,\theta_n}とおく。qnq_nはInI_nへの全射であるから、すべてのLnL_n一自由変数論理式に対する証人公理がTn+1T_{n+1}に属する。また、上の超限帰納法によりTn+1T_{n+1}はLn+1L_{n+1}において無矛盾である。

この操作をすべての非負整数nnについて反復し、

LH=⋃n<ωLn,Tω=⋃n<ωTnL^H=\bigcup_{n<\omega}L_n, \qquad T_\omega=\bigcup_{n<\omega}T_n

とおく。(Ln,Tn)n<ω(L_n,T_n)_{n<\omega}は言語と理論がともに増大する鎖であるから、補題 1.1によりTωT_\omegaはLHL^Hにおいて構文的に無矛盾である。LHL^Hの任意の論理式φ\varphiは有限個の記号だけを含むため、φ∈Form⁡(Ln)\varphi\in\operatorname{Form}(L_n)を満たす非負整数nnが存在する。したがって、その一自由変数論理式に対する証人公理はTn+1T_{n+1}で追加される。ゆえにTωT_\omegaは Henkin 理論である。

各nnについてθn≤κ\theta_n\le\kappaであるから、各段階の新定数と証人公理は高々κ\kappa個である。系 2.2により∣LH∣≤κ|L^H|\le\kappaである。TωT_\omegaはTTと、可算個の段階で加えた高々κ\kappa個ずつの証人公理との和集合である。§E1.22 系 3.3による∣ω×κ∣=κ|\omega\times\kappa|=\kappaと∣T∣≤κ|T|\le\kappaから両者のタグ付き和はκ×2\kappa\times 2へ単射する。再び同じ系を用いると∣κ×2∣=κ|\kappa\times2|=\kappaであるから、∣Tω∣≤κ|T_\omega|\le\kappaも従う。▨

一段階だけでは、その段階で加えた定数を含む新しい論理式の証人公理が不足する。可算段階の反復は、各論理式が有限個の記号しか含まないことと組み合わせることで、この不足を解消する。

5 Lindenbaum の補題

定義 5.1.LL理論SSが LLにおいて極大無矛盾 (maximally consistent theory in L) であるとは、SSがLLにおいて構文的に無矛盾であり、S⊊S′⊆Sent⁡(L)S\subsetneq S'\subseteq\operatorname{Sent}(L)を満たしLLにおいて構文的に無矛盾な理論S′S'が存在しないことをいう。言語が文脈から定まる場合には、単に極大無矛盾であるという。

定理 5.2 (Lindenbaum の補題). 集合サイズの言語LLにおける任意の構文的に無矛盾な理論SSは、極大無矛盾なLL理論へ拡大することができる。この存在証明では Zorn の補題、したがって選択公理を用いる。

証明.LLにおいて構文的に無矛盾でありSSを含むLL理論の全体を、包含関係で順序付ける。この順序集合はSSを含むので空でない。空でない鎖については、鎖の各要素に同じ言語LLを対応させると補題 1.1の言語が一定である特別な場合にあたるので、その合併はLLにおいて構文的に無矛盾である。鎖の各要素がSSを含むので合併もSSを含む。したがって合併はこの順序集合に属し、鎖の上界である。空の鎖についてはSS自身が上界である。§E1.20 定理 2.1 (3)の Zorn の補題を適用すると極大元S∗S^*が存在する。S∗S^*は定義どおり極大無矛盾なLL理論である。▨

補題 5.3.SSを極大無矛盾な理論とし、σ,τ\sigma,\tauを文とする。このとき、次が成り立つ。

  1. S⊢σS\vdash\sigmaであることとσ∈S\sigma\in Sであることは同値である。
  2. σ\sigmaと¬σ\neg\sigmaのちょうど一方がSSに属する。
  3. σ→τ∈S\sigma\to\tau\in Sであることと、σ∉S\sigma\notin Sまたはτ∈S\tau\in Sであることは同値である。

証明.S⊢σS\vdash\sigmaかつσ∉S\sigma\notin Sとする。S∪{σ}S\cup\{\sigma\}から矛盾が導かれれば、その有限導出で前提σ\sigmaを用いる各箇所へSSからのσ\sigmaの導出を代入して、SSから矛盾を導くことができる。したがってS∪{σ}S\cup\{\sigma\}は無矛盾であり、極大性に反する。ゆえにσ∈S\sigma\in Sである。逆向きは、前提は一行の導出になることから従う。

σ\sigmaと¬σ\neg\sigmaが両方属することは無矛盾性に反する。σ∉S\sigma\notin Sなら、極大性によりS∪{σ}S\cup\{\sigma\}は矛盾する。§E16.10 定理 5.1と§E16.10 補題 2.1が与える古典命題論理の派生則によりS⊢¬σS\vdash\neg\sigmaであり、(1)から¬σ∈S\neg\sigma\in Sである。したがってちょうど一方が属する。

σ→τ∈S\sigma\to\tau\in Sかつσ∈S\sigma\in Sなら、modus ponens と(1)によりτ∈S\tau\in Sである。したがってσ→τ∈S\sigma\to\tau\in Sならσ∉S\sigma\notin Sまたはτ∈S\tau\in Sである。逆にτ∈S\tau\in Sなら、§E16.10 定義 1.1の論理公理スキーマ (H1) の置換例τ→(σ→τ)\tau\to(\sigma\to\tau)と modus ponens からS⊢σ→τS\vdash\sigma\to\tauである。σ∉S\sigma\notin Sなら(2)から¬σ∈S\neg\sigma\in Sである。§E16.10 補題 2.1 (5)が与えるσ→(¬σ→⊥ρ)\sigma\to(\neg\sigma\to\bot_\rho)と⊥ρ→τ\bot_\rho\to\tauを用いるとS∪{σ}⊢τS\cup\{\sigma\}\vdash\tauであり、§E16.10 定理 5.1によりS⊢σ→τS\vdash\sigma\to\tauである。(1)により、どちらの場合もσ→τ∈S\sigma\to\tau\in Sとなる。▨

6 完全な Henkin 理論

定理 6.1.LLを集合サイズの有限項言語、T⊆Sent⁡(L)T\subseteq\operatorname{Sent}(L)を構文的に無矛盾な理論とし、κ=max⁡(ℵ0,∣L∣,∣T∣)\kappa=\max(\aleph_0,|L|,|T|)とおく。このとき、拡大言語LHL^Hと理論THT^Hで、次を満たすものが存在する。

  1. T⊆TH⊆Sent⁡(LH)T\subseteq T^H\subseteq\operatorname{Sent}(L^H)である。
  2. THT^Hは極大無矛盾な Henkin 理論である。
  3. ∣LH∣≤κ|L^H|\le\kappa、∣Sent⁡(LH)∣≤κ|\operatorname{Sent}(L^H)|\le\kappa、∣TH∣≤κ|T^H|\le\kappaである。
  4. FV(φ)⊆{x}FV(\varphi)\subseteq\{x\}かつ∃xφ(x)∈TH\exists x\varphi(x)\in T^Hなら、ある Henkin 定数ccが存在してφ(c)∈TH\varphi(c)\in T^Hである。

証明.定理 4.2により、無矛盾な Henkin 理論Tω⊆Sent⁡(LH)T_\omega\subseteq\operatorname{Sent}(L^H)を得る。定理 5.2をLHL^Hの中で適用し、TωT_\omegaを極大無矛盾な理論THT^Hへ拡大する。証人公理はすでにTωT_\omegaに属するので、THT^Hにも属する。したがってTHT^Hは Henkin 理論である。

∃xφ(x)∈TH\exists x\varphi(x)\in T^Hとする。対応する証人公理∃xφ(x)→φ(c)\exists x\varphi(x)\to\varphi(c)もTHT^Hに属する。 modus ponens と補題 5.3の導出閉包によりφ(c)∈TH\varphi(c)\in T^Hである。濃度評価は系 2.2と補題 2.1から従う。▨

7 選択公理を用いた箇所

本記事では、選択公理を次の三箇所で用いた。

  1. §E1.21 定理 2.2を用いて、任意の記号集合、構文対象の集合、および理論に対し、それらと等濃な基数を取った。
  2. 定理 4.2で、各段階の一自由変数論理式の集合を§E1.21 定理 2.2が与える基数で添字付けした。
  3. 定理 5.2で、「選択公理と Zorn の補題」の§E1.20 定理 2.1が与える Zorn の補題を適用した。

§E1.22 定理 3.2と§E1.22 系 3.3の証明自体は選択公理を用いない。本記事がこれらを任意の集合の濃度へ適用するときに必要な選択公理は、第1項の基数の取り出しに含まれる。また、補題 2.1では、固定した全単射κ×κ→κ\kappa\times\kappa\to\kappaから有限再帰で全写像を定めるため、可算個の写像を選ぶ選択公理は用いない。

可算言語では文を明示的な列へ並べる証明も可能である。しかし、本記事の定理は可算言語を仮定しないため、可算列挙を一般の場合の証明として用いていない。

8 演習

問題 8.1.

  1. 無矛盾な理論の増大列の合併が無矛盾である証明で、導出が有限であることをどこで用いるか説明せよ。
  2. Henkin 証人を加える操作を一段階で終えることができない理由を説明せよ。
  3. 補題 3.2の証明が完全性定理を用いていないことを、使用した結果の一覧から確認せよ。
  4. κ\kappaを無限濃度とし、§E1.22 定理 3.2が与える全単射p:κ×κ→κp:\kappa\times\kappa\to\kappaを一つ固定する。ppから有限再帰でκ<ω\kappa^{<\omega}をω×κ\omega\times\kappaへ単射し、§E1.22 系 3.3を用いて∣κ<ω∣=κ|\kappa^{<\omega}|=\kappaを証明せよ。この構成が可算選択公理を必要としない理由も述べよ。
解答 (確認問題の解答).
  1. 合併から矛盾を導く二つの導出について、用いる前提が有限個であることと、現れる非論理記号が有限個であることの双方に用いる。前者により、用いたすべての前提を含む段階が存在する。後者により、その段階の言語が二つの導出に現れるすべての記号を含むようにすることができる。導出が無限列であれば、前提も記号も有限個であるとはかぎらず、一つの段階を選ぶ推論は成立しない。
  2. 一段階で加えた新定数を含む論理式は、段階の開始時の言語には属していない。その論理式に対する証人定数は次の段階で必要になる。各論理式は有限個の記号しか含まないため、可算段階のどこかで必ず処理される。
  3. 使用した結果は、§E16.10 定理 5.1、§E16.10 補題 2.1が与える古典命題論理の派生則、§E16.5 定義 2.3による存在量化子の略記の展開、および補題 3.1である。モデル存在定理と完全性定理は使用していない。
  4. e1e_1をκ\kappaの恒等写像とし、en+1(s,a)=p(en(s),a)e_{n+1}(s,a)=p(e_n(s),a)と定めると、有限帰納法によりen:κn→κe_n:\kappa^n\to\kappaはすべての正の整数nnについて全単射である。空列を(0,0)(0,0)へ送り、長さn>0n>0の列ssを(n,en(s))(n,e_n(s))へ送れば、長さのタグが異なる列を分離する単射κ<ω→ω×κ\kappa^{<\omega}\to\omega\times\kappaを得る。§E1.22 系 3.3により∣ω×κ∣=κ|\omega\times\kappa|=\kappaであり、逆向きにはα\alphaを長さ一の列(α)(\alpha)へ送る単射があるので、§E1.21 命題 2.5と順序数の大小の反対称性により∣κ<ω∣=κ|\kappa^{<\omega}|=\kappaである。各ene_nは一つのppから有限再帰で一意に定まるので、可算個の写像から一つずつ選ぶ操作はない。

▨

参考文献

  1. Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001.Henkin 定数、Lindenbaum の補題、およびモデル存在証明の扱いを参考にした。
  2. C. C. Chang and H. Jerome Keisler, Model Theory, 3rd ed., Dover Publications, 2012, originally published 1990.任意濃度の言語に対する完全性証明と Henkin 構成の扱いを参考にした。
  3. Thomas Jech, Set Theory, 3rd millennium ed., Springer Monographs in Mathematics, Springer, Berlin, 2003.選択公理、整列可能定理、および無限濃度の有限積の扱いを参考にした。

前提記事