原子論理式の場合
まずは原子論理式の場合について考える.実はこの場合が一番大変である.
強制言語の原子閉論理式の全体をALPで表す.即ち,ALPはτ,ϑ∈VPに対しτ∈ϑまたはτ=ϑの形の論理式全体の成す真クラスである.
P:forcing poset,p∈P,φ∈ALPに対し,関係p⊩∗φを次により定義する:
p⊩∗τ=ϑdef∀σ∈dom(τ)∪dom(ϑ) ∀q≤p,[q⊩∗σ∈τ↔q⊩∗σ∈ϑ]
p⊩∗π∈τdef{q:∃⟨σ,r⟩∈τ[q≤r∧q⊩∗π=σ]}がp以下で稠密
これがちゃんとした帰納法の定義になっていることを示すためには,どんな整礎関係についての帰納法なのかをはっきりさせなくてはならない.そこで,以下(p,φ)∈P×ALP上に整礎関係を定義を定義しよう.
x⊲ydefx∈trcl(y) とおく.P×ALP上の二項関係≺を次で定義する: (p,σ1∈τ1)≺(q,σ2=τ2)⇔(σ1⊲σ2∨σ1⊲τ2)∧(τ1=σ2∨τ1=τ2)(p,σ1=τ1)≺(q,σ2∈τ2)⇔σ2=σ2∧τ2⊲τ1(p,σ1=τ1)≺(q,σ2=τ2),(p,σ1∈τ1)≺(q,σ2∈τ2)
≺はleft-narrow
(set-like)な整礎関係である.
Proof. left-narrow性はPが集合であることから従う.そこで,x≺y→Γ(x)<Γ(y)となるようなrank関数Γ:P×ALPを定めることによって整礎性を示す.
まずρ:VP×VP→Onを,ρ(σ,τ):=max{rank(σ),rank(τ)}と定め,Γを次で定める: Γ(p,σ∈τ)={3ρ(σ,τ)3ρ(σ,τ)+2(rank(σ)<rank(τ))(rank(σ)≥rank(τ))Γ(p,σ=τ)=3ρ(σ,τ)+1 すると,簡単な場合分けによりΓがrank関数となっていることがわかる.
これにより,p∈Pとφ∈ALPに対しp⊩∗φがwell-definedであることはわかった.
原子論理式の場合に⊩∗と⊩が一致することを示したい.そのために,補助的な定義と補題を確認しておく.
φ∈ALPとする.
p⊩∗φ,q≤p⇒q⊩∗φ
p⊩∗φ⇔{q:q⊩∗φ}がp以下で稠密
Proof. (1)は定義から明らか.(2)の⇒は(1)から従うので,示すべきは(⇐)である.
≺に関する帰納法で示す.φ≡π∈τの時は,{q:A が q以下で稠密}がp以下で稠密なら,Aがp以下で稠密となることから明らか.φ≡τ=ϑの時を考える.
対偶を示そう.p⊩∗π=τとすると,定義を展開すれば, ¬[q⊩∗σ∈τ↔q⊩∗σ∈ϑ]
を満たすようなq≤pとσ∈dom(τ)∪dom(ϑ)が存在する.特にq⊩∗σ∈τかつq⊩∗σ∈ϑであるとして一般性を失わない.すると,帰納法の仮定から{r:r⊩∗σ∈ϑ}はq以下で稠密でない.よって∀s≤r[s⊩∗π∈ϑ]を満たすr≤qが存在する.(1)とr≤q⊩∗σ∈τより,∀s≤r[s⊩∗σ∈τ↮s⊩∗σ∈ϑ].よって{q:q⊩∗τ=ϑ}はp以下で稠密でない.
φ∈ALPに対し, p⊩∗¬φdef∀q≤p[q⊩∗φ]
φ∈ALPについて p⊩∗φ⇔∀q≤p[q⊩∗¬φ]
Proof. (⇒)は定義と先の補題の(1)より明らか.(⇐)は対偶が(2)と定義から従う.
p∈P∈M,G⊆P:M上P-ジェネリック,D⊆P:p以下で稠密,D∈Mとすると,
p∈G⇒G∩D=∅
Proof. D+:=D∪{q∈P:q⊥p}とおけば,D+は稠密である.定義より明らかにD+∈M.よってGのジェネリック性よりG∩D+=∅.ここでr∈G∩D+をとると,r,p∈Gよりr∥pとなるので,r∈D.
M⊨ZF−P:ctm,P∈M,G⊆P:M上P-ジェネリック,φ∈AL∩Mとする.
(p⊩∗φ)M∧p∈G⇒M[G]⊨φ
M[G]⊨φ⇒∃p∈G(p⊩∗φ)M
Proof. それぞれ≺に関する帰納法で示す.原子論理式の場合に関しては定義の方法から⊩∗は推移的モデルに対して絶対なので,以下相対化を落として考えよう.
p⊩∗τ=ϑの時.M[G]⊨τ⊆ϑが示せれば逆向きも同様に示せる.そこでσG∈τG,r∈Gとなるような⟨σ,r⟩∈τを取る.p,r∈Gよりq≤p,rでq∈Gを満たすものが取れる.すると注意1よりq⊩∗σ∈τとなる.また,⊩∗の定義よりq⊩∗σ∈τ↔q⊩∗σ∈ϑだったのでq⊩∗σ∈ϑが成立する.すると帰納法の仮定よりM[G]⊨σ∈ϑとなり,M[G]⊨τ⊆ϑが云えた.
p⊩∗π∈τの時.この時, D:={q:∃⟨σ,r⟩∈τ[q≤r∧q⊩∗π=σ]}
はp以下で稠密である.よって補題3よりq≤pで∃⟨σ,r⟩∈τ[q≤r∧q⊩∗π=σ],q∈Gを満たすものが取れる.よって帰納法の仮定よりM[G]⊨π=σである.Gはフィルターなのでr∈Gだから,以上と合わせてπG=σG∈τGとなり,M[G]⊨π∈τが云えた.
M[G]⊨π∈τの時.D={q:∃⟨σ,r⟩∈τ[q≤r∧q⊩∗π=σ]}がp以下で稠密となるようなp∈Gを見付けたい.定義より,⟨σ,r⟩∈τでσG=πGかつr∈Gを満たすような物が取れる.定義を展開すればM[G]⊨π=σであり,帰納法の仮定よりp⊩∗π=σを満たすようなp∈Gが取れる.Gがフィルターであることと補題 1
(1)からp≤rとして良い.すると補題 1 (2)よりDはp以下で稠密となり,p⊩∗π∈τとなる.
M[G]⊨τ=ϑの時.Dを以下のいずれか一つを満たすqの全体とする:
q⊩∗τ=ϑ
∃σ∈dom(τ)∪dom(ϑ)[q⊩∗σ∈τ∧q⊩∗σ∈/ϑ]
∃σ∈dom(τ)∪dom(ϑ)[q⊩∗σ∈/τ∧q⊩∗σ∈ϑ]
すると,DはPで稠密であり,特にD∈Mである.すると,Gはジェネリックなのでp∈G∩Dが取れる.pが(1)を満たせばOK.もし(2)を満たすとすると,p∈Gと(a)よりM[G]⊨σ∈τとなる.ここで,M[G]⊨τ=ϑよりこれらを合わせればM[G]⊨σ∈ϑ.すると帰納法の仮定よりq⊩∗σ∈ϑを満たすようなq∈Gを取ることが出来る.特にq≤pとしてよい.しかし,q≤p⊩∗σ∈/ϑより⊩∗の定義からq⊩∗σ∈ϑとならなくてはならないので矛盾.同様の議論により(3)も有り得ない.
M⊨ZF−P:c.t.m.,P∈M,φ∈ALP∩M⟹p⊩P,Mφ⇔(p⊩P∗φ)M
Proof.
前回とおなじく相対化は無視して議論を進めることが出来る. (⇐)は補題 1
(a)より直ちに従うので, (⇒)を示す.そこでp⊩φかつp⊩∗φとする.この時補題2よりq⊩∗¬φを満たすq≤pが存在する.すると定義より∀r≤q[r⊩∗φ]となる.ここでq∈Gを満たすジェネリックフィルターを取る.この時p≥qよりp∈Gなので,仮定よりM[G]⊨φを満たす.すると,補題1 (b)よりr∈Gでr⊩∗φを満たすものが取れ,Gがフィルターであることから特にr≤qとできる.するとr⊩∗¬φとなり矛盾.
一般の論理式について
原子論理式に関しての定義は済んだので,一般の強制言語の論理式に対して⊩∗ を定義していこう.
p∈P∈M⊨ZF−P,φ,ψ∈FLPについて,以下のように帰納的にp⊩∗φを定める:
φ∈ALPの時は定義2と同じ.
p⊩∗φ∧ψdefp⊩∗φかつp⊩∗ψ
p⊩∗¬φdef∀q≤p[q⊩∗φ]
p⊩∗φ→ψdef¬∃q≥p[q⊩∗φ∧q⊩∗¬ψ]
p⊩∗φ∨ψdef{q:[q⊩∗φ]∨[q⊩∗ψ]}がp以下で稠密
p⊩∗∀xφ(x)def∀τ∈VPp⊩∗φ(τ)
p⊩∗∃xφ(x)def{q:∃τ∈VPq⊩∗φ(τ)}がp以下で稠密
ここで,(3)の定義は定義4と整合的である.また,∀,∃の定義は,∧,∨の定義の一般化と見做せる.
この「帰納的」定義を注意深くみてみると,(6)や(7)の定義では,各τ∈VPについてφ(τ)の形のFLP閉論理式全体について帰納法を回している.これは真クラスなのでVの中ではどう頑張っても定義出来ないことがわかる.即ち,上の⊩∗の定義はメタ理論における定義図式であって,p⊩∗φ⇔Ψ(p,φ)を満たすような一つの論理式が存在するのではない.つまり,各φ(x)∈FLPに対して,p⊩∗φ(ϰ)を表す論理式Forcesφ(p,ϰ)を帰納的に作る方法が,論理式の長さに関する帰納法で与えられているのだ.我々の目的は⊩に関するDefinability
lemmaを確立することだから,各φに対してp⊩φを表す論理式を別個に書くことができれば良いので,⊩∗がVの内部で定義出来なくても問題はないのである.
このように定義すれば,今までの原子論理式に対する命題を一般の強制言語の論理式に拡張出来る.上の定義は,¬が与えられれば同値変形だけで出て来るので,以下では必要最低限の場合だけ証明することにする:
φ∈FLPに対し,
p⊩∗φ,q≤p⇒q⊩∗φ
p⊩∗φ⇔{q:q⊩∗φ}がp以下で稠密
p⊩∗φ⇔∀q≤p[q⊩∗¬φ]
p⊩∗φかつp⊩∗¬φとなることは有り得ない.
Proof.
(c)(d)は(a)(b)から従い,(a)は定義より明らか.原子論理式の場合と同様に(b)の(⇐)だけ帰納法により示す.
φ≡∀xψ(x)の時.{q:q⊩∗∀xψ(x)}がp以下で稠密だとする.定義を展開すれば,
∀q≤p∃r≤q∀τ∈VP[r⊩∗ψ(τ)]
となる.特にこれから各τ∈VPについて{q:q⊩∗ψ(τ)}はp以下で稠密となる.よって帰納法の仮定より∀τ∈VPp⊩∗ψ(τ)となり,定義からp⊩∗∀xφ(x)となる.
φ≡¬ψの時.対偶を示す.p⊩∗¬ψとすると,定義から∃q≤p[q⊩∗ψ]であり,(a)より∀r≤q[r⊩∗ψ]となる.よって{s:s⊩∗¬ψ}はp以下で稠密でない.
φ≡ψ∨ϑの時.D={q:q⊩∗ψ∨ϑ}がp以下で稠密だとする.このときもう少し定義を展開すると,{q:{r:[r⊩∗ψ]∨[r⊩∗ϑ]} が q 以下で稠密}がp以下で稠密である.稠密性の定義よりこれは単に{r:[r⊩∗ψ]∨[r⊩∗ϑ]}がp以下で稠密であるということである.
いよいよ,一般のφについて⊩∗をモデルと結び付ける補題を証明する:
M⊨ZF−P:ctm,P∈M,G⊆P:M上P-ジェネリック,φ∈FL∩Mとする.
(p⊩∗φ)M∧p∈G⇒M[G]⊨φ
M[G]⊨φ⇒∃p∈G(p⊩∗φ)M
Proof. 構造に関する帰納法により,(a)
(b)の二つを同時に証明する.L(φ)により「φについて(a)
(b)が成立する」ことを表す.
以上を使えば,原子論理式の時と同様にして⊩との関係を証明できる:
M⊨ZF−P:c.t.m.,P∈M,φ∈FLP∩M⟹p⊩φ⇔(p⊩∗φ)M
ここまでくれば,Definability lemmaとTruth
lemmaの証明は簡単である:
Truth lemmaとDefinability lemmaの証明. Truth
lemmaは補題8および補題7の(b)から明らか.Definability
lemmaについても,補題8より{(P,≤,1,p,κ):⋯ p⊩φ(ϰ)}はM内で定義可能.
実は,後程示すが「M⊨ZFCでp⊩∃xφ(x)ならばp⊩φ(τ)を満たすτ∈MPが存在する」という定理(極大原理)がある.これを使えば∃に関する⊩∗の定義を簡略化出来そうな気もするが,その極大原理の証明にここでの議論を使っているので循環論法になってしまう.また,Mが必ずしもACを満たさない場合に使えなくなってしまうので,ここでは上の定義を用いた.