Theory Forcing_Theorems
section‹The Forcing Theorems›
theory Forcing_Theorems
imports
Cohen_Posets_Relative
Forces_Definition
Names
begin
context forcing_data1
begin
subsection‹The forcing relation in context›
lemma separation_forces :
assumes
fty: "φ∈formula" and
far: "arity(φ)≤length(env)" and
envty: "env∈list(M)"
shows
"separation(##M,λp. (p ⊩ φ env))"
using separation_ax arity_forces far fty envty arity_forces_le
transitivity[of _ ℙ]
by simp
lemma Collect_forces :
assumes
"φ∈formula" and
"arity(φ)≤length(env)" and
"env∈list(M)"
shows
"{p∈ℙ . p ⊩ φ env} ∈ M"
using assms separation_forces separation_closed
by simp
lemma forces_mem_iff_dense_below: "p∈ℙ ⟹ p forces⇩a (t1 ∈ t2) ⟷ dense_below(
{q∈ℙ. ∃s. ∃r. r∈ℙ ∧ ⟨s,r⟩ ∈ t2 ∧ q≼r ∧ q forces⇩a (t1 = s)}
,p)"
using def_forces_mem[of p t1 t2] by blast
subsection‹Kunen 2013, Lemma IV.2.37(a)›
lemma strengthening_eq:
assumes "p∈ℙ" "r∈ℙ" "r≼p" "p forces⇩a (t1 = t2)"
shows "r forces⇩a (t1 = t2)"
using assms def_forces_eq[of _ t1 t2] leq_transD by blast
subsection‹Kunen 2013, Lemma IV.2.37(a)›
lemma strengthening_mem:
assumes "p∈ℙ" "r∈ℙ" "r≼p" "p forces⇩a (t1 ∈ t2)"
shows "r forces⇩a (t1 ∈ t2)"
using assms forces_mem_iff_dense_below dense_below_under by auto
subsection‹Kunen 2013, Lemma IV.2.37(b)›
lemma density_mem:
assumes "p∈ℙ"
shows "p forces⇩a (t1 ∈ t2) ⟷ dense_below({q∈ℙ. q forces⇩a (t1 ∈ t2)},p)"
proof
assume "p forces⇩a (t1 ∈ t2)"
with assms
show "dense_below({q∈ℙ. q forces⇩a (t1 ∈ t2)},p)"
using forces_mem_iff_dense_below strengthening_mem[of p] ideal_dense_below by auto
next
assume "dense_below({q ∈ ℙ . q forces⇩a ( t1 ∈ t2)}, p)"
with assms
have "dense_below({q∈ℙ.
dense_below({q'∈ℙ. ∃s r. r ∈ ℙ ∧ ⟨s,r⟩∈t2 ∧ q'≼r ∧ q' forces⇩a (t1 = s)},q)
},p)"
using forces_mem_iff_dense_below by simp
with assms
show "p forces⇩a (t1 ∈ t2)"
using dense_below_dense_below forces_mem_iff_dense_below[of p t1 t2] by blast
qed
lemma aux_density_eq:
assumes
"dense_below(
{q'∈ℙ. ∀q. q∈ℙ ∧ q≼q' ⟶ q forces⇩a (s ∈ t1) ⟷ q forces⇩a (s ∈ t2)}
,p)"
"q forces⇩a (s ∈ t1)" "q∈ℙ" "p∈ℙ" "q≼p"
shows
"dense_below({r∈ℙ. r forces⇩a (s ∈ t2)},q)"
proof
fix r
assume "r∈ℙ" "r≼q"
moreover from this and ‹p∈ℙ› ‹q≼p› ‹q∈ℙ›
have "r≼p"
using leq_transD by simp
moreover
note ‹q forces⇩a (s ∈ t1)› ‹dense_below(_,p)› ‹q∈ℙ›
ultimately
obtain q1 where "q1≼r" "q1∈ℙ" "q1 forces⇩a (s ∈ t2)"
using strengthening_mem[of q _ s t1] refl_leq leq_transD[of _ r q] by blast
then
show "∃d∈{r ∈ ℙ . r forces⇩a ( s ∈ t2)}. d ∈ ℙ ∧ d≼ r"
by blast
qed
lemma density_eq:
assumes "p∈ℙ"
shows "p forces⇩a (t1 = t2) ⟷ dense_below({q∈ℙ. q forces⇩a (t1 = t2)},p)"
proof
assume "p forces⇩a (t1 = t2)"
with ‹p∈ℙ›
show "dense_below({q∈ℙ. q forces⇩a (t1 = t2)},p)"
using strengthening_eq ideal_dense_below by auto
next
assume "dense_below({q∈ℙ. q forces⇩a (t1 = t2)},p)"
{
fix s q
let ?D1="{q'∈ℙ. ∀s∈domain(t1) ∪ domain(t2). ∀q. q ∈ ℙ ∧ q≼q' ⟶
q forces⇩a (s ∈ t1)⟷q forces⇩a (s ∈ t2)}"
let ?D2="{q'∈ℙ. ∀q. q∈ℙ ∧ q≼q' ⟶ q forces⇩a (s ∈ t1) ⟷ q forces⇩a (s ∈ t2)}"
assume "s∈domain(t1) ∪ domain(t2)"
then
have "?D1⊆?D2" by blast
with ‹dense_below(_,p)›
have "dense_below({q'∈ℙ. ∀s∈domain(t1) ∪ domain(t2). ∀q. q ∈ ℙ ∧ q≼q' ⟶
q forces⇩a (s ∈ t1)⟷q forces⇩a (s ∈ t2)},p)"
using dense_below_cong'[OF ‹p∈ℙ› def_forces_eq[of _ t1 t2]] by simp
with ‹p∈ℙ› ‹?D1⊆?D2›
have "dense_below({q'∈ℙ. ∀q. q∈ℙ ∧ q≼q' ⟶
q forces⇩a (s ∈ t1) ⟷ q forces⇩a (s ∈ t2)},p)"
using dense_below_mono by simp
moreover from this
have "dense_below({q'∈ℙ. ∀q. q∈ℙ ∧ q≼q' ⟶
q forces⇩a (s ∈ t2) ⟷ q forces⇩a (s ∈ t1)},p)"
by blast
moreover
assume "q ∈ ℙ" "q≼p"
moreover
note ‹p∈ℙ›
ultimately
have "q forces⇩a (s ∈ t1) ⟹ dense_below({r∈ℙ. r forces⇩a (s ∈ t2)},q)"
"q forces⇩a (s ∈ t2) ⟹ dense_below({r∈ℙ. r forces⇩a (s ∈ t1)},q)"
using aux_density_eq by simp_all
then
have "q forces⇩a ( s ∈ t1) ⟷ q forces⇩a ( s ∈ t2)"
using density_mem[OF ‹q∈ℙ›] by blast
}
with ‹p∈ℙ›
show "p forces⇩a (t1 = t2)" using def_forces_eq by blast
qed
subsection‹Kunen 2013, Lemma IV.2.38›
lemma not_forces_neq:
assumes "p∈ℙ"
shows "p forces⇩a (t1 = t2) ⟷ ¬ (∃q∈ℙ. q≼p ∧ q forces⇩a (t1 ≠ t2))"
using assms density_eq unfolding forces_neq_def by blast
lemma not_forces_nmem:
assumes "p∈ℙ"
shows "p forces⇩a (t1 ∈ t2) ⟷ ¬ (∃q∈ℙ. q≼p ∧ q forces⇩a (t1 ∉ t2))"
using assms density_mem unfolding forces_nmem_def by blast
subsection‹The relation of forcing and atomic formulas›
lemma Forces_Equal:
assumes
"p∈ℙ" "t1∈M" "t2∈M" "env∈list(M)" "nth(n,env) = t1" "nth(m,env) = t2" "n∈nat" "m∈nat"
shows
"(p ⊩ Equal(n,m) env) ⟷ p forces⇩a (t1 = t2)"
using assms sats_forces_Equal forces_eq_abs transitivity
by simp
lemma Forces_Member:
assumes
"p∈ℙ" "t1∈M" "t2∈M" "env∈list(M)" "nth(n,env) = t1" "nth(m,env) = t2" "n∈nat" "m∈nat"
shows
"(p ⊩ Member(n,m) env) ⟷ p forces⇩a (t1 ∈ t2)"
using assms sats_forces_Member forces_mem_abs transitivity
by simp
lemma Forces_Neg:
assumes
"p∈ℙ" "env ∈ list(M)" "φ∈formula"
shows
"(p ⊩ Neg(φ) env) ⟷ ¬(∃q∈M. q∈ℙ ∧ q≼p ∧ (q ⊩ φ env))"
using assms sats_forces_Neg transitivity pair_in_M_iff leq_abs
by simp
subsection‹The relation of forcing and connectives›
lemma Forces_Nand:
assumes
"p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula"
shows
"(p ⊩ Nand(φ,ψ) env) ⟷ ¬(∃q∈M. q∈ℙ ∧ q≼p ∧ (q ⊩ φ env) ∧ (q ⊩ ψ env))"
using assms sats_forces_Nand transitivity pair_in_M_iff leq_abs by simp
lemma Forces_And_aux:
assumes
"p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula"
shows
"p ⊩ And(φ,ψ) env ⟷
(∀q∈M. q∈ℙ ∧ q≼p ⟶ (∃r∈M. r∈ℙ ∧ r≼q ∧ (r ⊩ φ env) ∧ (r ⊩ ψ env)))"
unfolding And_def using assms Forces_Neg Forces_Nand by (auto simp only:)
lemma Forces_And_iff_dense_below:
assumes
"p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula"
shows
"(p ⊩ And(φ,ψ) env) ⟷ dense_below({r∈ℙ. (r ⊩ φ env) ∧ (r ⊩ ψ env) },p)"
unfolding dense_below_def using Forces_And_aux assms
by (auto dest:transitivity[OF _ P_in_M]; rename_tac q; drule_tac x=q in bspec)+
lemma Forces_Forall:
assumes
"p∈ℙ" "env ∈ list(M)" "φ∈formula"
shows
"(p ⊩ Forall(φ) env) ⟷ (∀x∈M. (p ⊩ φ ([x] @ env)))"
using sats_forces_Forall assms transitivity[OF _ P_in_M]
by simp
bundle some_rules = elem_of_val_pair [dest]
context
includes some_rules
begin
lemma elem_of_valI: "∃θ. ∃p∈ℙ. p∈G ∧ ⟨θ,p⟩∈π ∧ val(G,θ) = x ⟹ x∈val(G,π)"
by (subst def_val, auto)
lemma GenExt_iff: "x∈M[G] ⟷ (∃τ∈M. x = val(G,τ))"
unfolding GenExt_def by simp
end
end
context G_generic1
begin
subsection‹Kunen 2013, Lemma IV.2.29›
lemma generic_inter_dense_below:
assumes "D∈M" "dense_below(D,p)" "p∈G"
shows "D ∩ G ≠ 0"
proof -
let ?D="{q∈ℙ. p⊥q ∨ q∈D}"
have "dense(?D)"
proof
fix r
assume "r∈ℙ"
show "∃d∈{q ∈ ℙ . p ⊥ q ∨ q ∈ D}. d ≼ r"
proof (cases "p ⊥ r")
case True
with ‹r∈ℙ›
show ?thesis using refl_leq[of r] by (intro bexI) (blast+)
next
case False
then
obtain s where "s∈ℙ" "s≼p" "s≼r" by blast
with assms ‹r∈ℙ›
show ?thesis
using dense_belowD[OF assms(2), of s] leq_transD[of _ s r]
by blast
qed
qed
have "?D⊆ℙ" by auto
let ?d_fm="⋅⋅¬compat_in_fm(1, 2, 3, 0) ⋅ ∨ ⋅0 ∈ 4⋅⋅"
from ‹p∈G›
have "p∈M"
using G_subset_M subsetD by simp
moreover
have "?d_fm∈formula" by simp
moreover
have "arity(?d_fm) = 5"
by (auto simp add: arity)
moreover from ‹D∈M› ‹p∈M›
have "(M, [q,ℙ,leq,p,D] ⊨ ?d_fm) ⟷ (¬ is_compat_in(##M,ℙ,leq,p,q) ∨ q∈D)"
if "q∈M" for q
using that sats_compat_in_fm zero_in_M
by simp
moreover from ‹p∈M›
have "(¬ is_compat_in(##M,ℙ,leq,p,q) ∨ q∈D) ⟷ p⊥q ∨ q∈D" if "q∈M" for q
unfolding compat_def
using that compat_in_abs
by simp
ultimately
have "?D∈M"
using Collect_in_M[of ?d_fm "[ℙ,leq,p,D]"] ‹D∈M›
by simp
note asm = ‹dense(?D)› ‹?D⊆ℙ› ‹?D∈M›
obtain x where "x∈G" "x∈?D"
using M_generic_denseD[OF asm]
by force
moreover from this
have "x∈D"
using M_generic_compatD[OF _ ‹p∈G›, of x] refl_leq compatI[of _ p x]
by force
ultimately
show ?thesis by auto
qed
subsection‹Auxiliary results for Lemma IV.2.40(a)›
lemma (in forcing_data1) IV240a_mem_Collect:
assumes
"π∈M" "τ∈M"
shows
"{q∈ℙ. ∃σ. ∃r. r∈ℙ ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩a (π = σ)}∈M"
proof -
let ?rel_pred= "λM x a1 a2 a3 a4. ∃σ[M]. ∃r[M]. ∃σr[M].
r∈a1 ∧ pair(M,σ,r,σr) ∧ σr∈a4 ∧ is_leq(M,a2,x,r) ∧ is_forces_eq'(M,a1,a2,x,a3,σ)"
let ?φ="Exists(Exists(Exists(And(Member(1,4),And(pair_fm(2,1,0),
And(Member(0,7),And(is_leq_fm(5,3,1),forces_eq_fm(4,5,3,6,2))))))))"
have "σ∈M ∧ r∈M" if "⟨σ, r⟩ ∈ τ" for σ r
using that ‹τ∈M› pair_in_M_iff transitivity[of "⟨σ,r⟩" τ] by simp
then
have "?rel_pred(##M,q,ℙ,leq,π,τ) ⟷ (∃σ. ∃r. r∈ℙ ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩a (π = σ))"
if "q∈M" for q
unfolding forces_eq_def
using assms that leq_abs forces_eq'_abs pair_in_M_iff
by auto
moreover
have "(M, [q,ℙ,leq,π,τ] ⊨ ?φ) ⟷ ?rel_pred(##M,q,ℙ,leq,π,τ)" if "q∈M" for q
using assms that sats_forces_eq_fm sats_is_leq_fm zero_in_M
by simp
moreover
have "?φ∈formula" by simp
moreover
have "arity(?φ)=5"
using arity_forces_eq_fm
by (simp add:ord_simp_union arity)
ultimately
show ?thesis
unfolding forces_eq_def using assms Collect_in_M[of ?φ "[ℙ,leq,π,τ]"]
by simp
qed
lemma IV240a_mem:
assumes
"p∈G" "π∈M" "τ∈M" "p forces⇩a (π ∈ τ)"
"⋀q σ. q∈ℙ ⟹ q∈G ⟹ σ∈domain(τ) ⟹ q forces⇩a (π = σ) ⟹
val(G,π) = val(G,σ)"
shows
"val(G,π)∈val(G,τ)"
proof (intro elem_of_valI)
let ?D="{q∈ℙ. ∃σ. ∃r. r∈ℙ ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩a (π = σ)}"
from ‹p∈G›
have "p∈ℙ" by blast
moreover
note ‹π∈M› ‹τ∈M›
ultimately
have "?D ∈ M" using IV240a_mem_Collect by simp
moreover from assms ‹p∈ℙ›
have "dense_below(?D,p)"
using forces_mem_iff_dense_below by simp
moreover
note ‹p∈G›
ultimately
obtain q where "q∈G" "q∈?D"
using generic_inter_dense_below[of ?D p] by blast
then
obtain σ r where "r∈ℙ" "⟨σ,r⟩ ∈ τ" "q≼r" "q forces⇩a (π = σ)" by blast
moreover from this and ‹q∈G› assms
have "r ∈ G" "val(G,π) = val(G,σ)" by blast+
ultimately
show "∃ σ. ∃p∈ℙ. p ∈ G ∧ ⟨σ, p⟩ ∈ τ ∧ val(G, σ) = val(G, π)" by auto
qed
lemma refl_forces_eq:"p∈ℙ ⟹ p forces⇩a (x = x)"
using def_forces_eq by simp
lemma forces_memI: "⟨σ,r⟩∈τ ⟹ p∈ℙ ⟹ r∈ℙ ⟹ p≼r ⟹ p forces⇩a (σ ∈ τ)"
using refl_forces_eq[of _ σ] leq_transD refl_leq
by (blast intro:forces_mem_iff_dense_below[THEN iffD2])
lemma IV240a_eq_1st_incl:
includes some_rules
assumes
"p∈G" "p forces⇩a (τ = θ)"
and
IH:"⋀q σ. q∈ℙ ⟹ q∈G ⟹ σ∈domain(τ) ∪ domain(θ) ⟹
(q forces⇩a (σ ∈ τ) ⟶ val(G,σ) ∈ val(G,τ)) ∧
(q forces⇩a (σ ∈ θ) ⟶ val(G,σ) ∈ val(G,θ))"
shows
"val(G,τ) ⊆ val(G,θ)"
proof
fix x
assume "x∈val(G,τ)"
then
obtain σ r where "⟨σ,r⟩∈τ" "r∈G" "val(G,σ)=x" by blast
moreover from this and ‹p∈G›
obtain q where "q∈G" "q≼p" "q≼r" by force
moreover from this and ‹p∈G›
have "q∈ℙ" "p∈ℙ" by blast+
moreover from calculation
have "q forces⇩a (σ ∈ τ)"
using forces_memI by auto
moreover
note ‹p forces⇩a (τ = θ)›
ultimately
have "q forces⇩a (σ ∈ θ)"
using def_forces_eq by auto
with ‹q∈ℙ› ‹q∈G› IH[of q σ] ‹⟨σ,r⟩∈τ› ‹val(G,σ) = x›
show "x∈val(G,θ)" by blast
qed
lemma IV240a_eq_2nd_incl:
includes some_rules
assumes
"p∈G" "p forces⇩a (τ = θ)"
and
IH:"⋀q σ. q∈ℙ ⟹ q∈G ⟹ σ∈domain(τ) ∪ domain(θ) ⟹
(q forces⇩a (σ ∈ τ) ⟶ val(G,σ) ∈ val(G,τ)) ∧
(q forces⇩a (σ ∈ θ) ⟶ val(G,σ) ∈ val(G,θ))"
shows
"val(G,θ) ⊆ val(G,τ)"
proof
fix x
assume "x∈val(G,θ)"
then
obtain σ r where "⟨σ,r⟩∈θ" "r∈G" "val(G,σ)=x" by blast
moreover from this and ‹p∈G›
obtain q where "q∈G" "q≼p" "q≼r" by force
moreover from this and ‹p∈G›
have "q∈ℙ" "p∈ℙ" by blast+
moreover from calculation
have "q forces⇩a (σ ∈ θ)"
using forces_memI by auto
moreover
note ‹p forces⇩a (τ = θ)›
ultimately
have "q forces⇩a (σ ∈ τ)"
using def_forces_eq by auto
with ‹q∈ℙ› ‹q∈G› IH[of q σ] ‹⟨σ,r⟩∈θ› ‹val(G,σ) = x›
show "x∈val(G,τ)" by blast
qed
lemma IV240a_eq:
includes some_rules
assumes
"p∈G" "p forces⇩a (τ = θ)"
and
IH:"⋀q σ. q∈ℙ ⟹ q∈G ⟹ σ∈domain(τ) ∪ domain(θ) ⟹
(q forces⇩a (σ ∈ τ) ⟶ val(G,σ) ∈ val(G,τ)) ∧
(q forces⇩a (σ ∈ θ) ⟶ val(G,σ) ∈ val(G,θ))"
shows
"val(G,τ) = val(G,θ)"
using IV240a_eq_1st_incl[OF assms] IV240a_eq_2nd_incl[OF assms] IH by blast
subsection‹Induction on names›
lemma (in forcing_data1) core_induction:
assumes
"⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(θ)⟧ ⟹ Q(0,τ,σ,q)⟧ ⟹ Q(1,τ,θ,p)"
"⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ Q(1,σ,τ,q) ∧ Q(1,σ,θ,q)⟧ ⟹ Q(0,τ,θ,p)"
"ft ∈ 2" "p ∈ ℙ"
shows
"Q(ft,τ,θ,p)"
proof -
{
fix ft p τ θ
have "Transset(eclose({τ,θ}))" (is "Transset(?e)")
using Transset_eclose by simp
have "τ ∈ ?e" "θ ∈ ?e"
using arg_into_eclose by simp_all
moreover
assume "ft ∈ 2" "p ∈ ℙ"
ultimately
have "⟨ft,τ,θ,p⟩∈ 2×?e×?e×ℙ" (is "?a∈2×?e×?e×ℙ") by simp
then
have "Q(ftype(?a), name1(?a), name2(?a), cond_of(?a))"
using core_induction_aux[of ?e ℙ Q ?a,OF ‹Transset(?e)› assms(1,2) ‹?a∈_›]
by (clarify) (blast)
then have "Q(ft,τ,θ,p)" by (simp add:components_simp)
}
then show ?thesis using assms by simp
qed
lemma (in forcing_data1) forces_induction_with_conds:
assumes
"⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(θ)⟧ ⟹ Q(q,τ,σ)⟧ ⟹ R(p,τ,θ)"
"⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ R(q,σ,τ) ∧ R(q,σ,θ)⟧ ⟹ Q(p,τ,θ)"
"p ∈ ℙ"
shows
"Q(p,τ,θ) ∧ R(p,τ,θ)"
proof -
let ?Q="λft τ θ p. (ft = 0 ⟶ Q(p,τ,θ)) ∧ (ft = 1 ⟶ R(p,τ,θ))"
from assms(1)
have "⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(θ)⟧ ⟹ ?Q(0,τ,σ,q)⟧ ⟹ ?Q(1,τ,θ,p)"
by simp
moreover from assms(2)
have "⋀τ θ p. p ∈ ℙ ⟹ ⟦⋀q σ. ⟦q∈ℙ ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ ?Q(1,σ,τ,q) ∧ ?Q(1,σ,θ,q)⟧ ⟹ ?Q(0,τ,θ,p)"
by simp
moreover
note ‹p∈ℙ›
ultimately
have "?Q(ft,τ,θ,p)" if "ft∈2" for ft
by (rule core_induction[OF _ _ that, of ?Q])
then
show ?thesis by auto
qed
lemma (in forcing_data1) forces_induction:
assumes
"⋀τ θ. ⟦⋀σ. σ∈domain(θ) ⟹ Q(τ,σ)⟧ ⟹ R(τ,θ)"
"⋀τ θ. ⟦⋀σ. σ∈domain(τ) ∪ domain(θ) ⟹ R(σ,τ) ∧ R(σ,θ)⟧ ⟹ Q(τ,θ)"
shows
"Q(τ,θ) ∧ R(τ,θ)"
proof (intro forces_induction_with_conds[OF _ _ one_in_P ])
fix τ θ p
assume "q ∈ ℙ ⟹ σ ∈ domain(θ) ⟹ Q(τ, σ)" for q σ
with assms(1)
show "R(τ,θ)"
using one_in_P by simp
next
fix τ θ p
assume "q ∈ ℙ ⟹ σ ∈ domain(τ) ∪ domain(θ) ⟹ R(σ,τ) ∧ R(σ,θ)" for q σ
with assms(2)
show "Q(τ,θ)"
using one_in_P by simp
qed
subsection‹Lemma IV.2.40(a), in full›
lemma IV240a:
shows
"(τ∈M ⟶ θ∈M ⟶ (∀p∈G. p forces⇩a (τ = θ) ⟶ val(G,τ) = val(G,θ))) ∧
(τ∈M ⟶ θ∈M ⟶ (∀p∈G. p forces⇩a (τ ∈ θ) ⟶ val(G,τ) ∈ val(G,θ)))"
(is "?Q(τ,θ) ∧ ?R(τ,θ)")
proof (intro forces_induction[of ?Q ?R] impI)
fix τ θ
assume "τ∈M" "θ∈M" "σ∈domain(θ) ⟹ ?Q(τ,σ)" for σ
moreover from this
have "σ∈domain(θ) ⟹ q forces⇩a (τ = σ) ⟹ val(G, τ) = val(G, σ)"
if "q∈ℙ" "q∈G" for q σ
using that domain_closed[of θ] transitivity by auto
ultimately
show "∀p∈G. p forces⇩a (τ ∈ θ) ⟶ val(G,τ) ∈ val(G,θ)"
using IV240a_mem domain_closed transitivity by simp
next
fix τ θ
assume "τ∈M" "θ∈M" and d:"σ ∈ domain(τ) ∪ domain(θ) ⟹ ?R(σ,τ) ∧ ?R(σ,θ)" for σ
moreover from this
have IH':"(q forces⇩a (σ ∈ τ) ⟶ val(G, σ) ∈ val(G, τ)) ∧
(q forces⇩a (σ ∈ θ) ⟶ val(G, σ) ∈ val(G, θ))"
if "σ ∈ domain(τ) ∪ domain(θ)" "q∈G" for q σ
proof -
from d that
have A:"?R(σ,τ)" "?R(σ,θ)"
by auto
from ‹τ∈_› ‹θ∈M› ‹q∈G› ‹σ∈_›
show ?thesis
using transitivity[of σ] domain_closed A[rule_format,of q]
by auto
qed
show "∀p∈G. p forces⇩a (τ = θ) ⟶ val(G,τ) = val(G,θ)"
using IV240a_eq[OF _ _ IH'] by simp
qed
subsection‹Lemma IV.2.40(b)›
lemma IV240b_mem:
includes some_rules
assumes
"val(G,π)∈val(G,τ)" "π∈M" "τ∈M"
and
IH:"⋀σ. σ∈domain(τ) ⟹ val(G,π) = val(G,σ) ⟹
∃p∈G. p forces⇩a (π = σ)"
shows
"∃p∈G. p forces⇩a (π ∈ τ)"
proof -
from ‹val(G,π)∈val(G,τ)›
obtain σ r where "r∈G" "⟨σ,r⟩∈τ" "val(G,π) = val(G,σ)" by auto
moreover from this and IH
obtain p' where "p'∈G" "p' forces⇩a (π = σ)" by blast
ultimately
obtain p where "p≼r" "p≼p'" "p∈G" "p forces⇩a (π = σ)"
using M_generic_compatD strengthening_eq[of p'] M_genericD by auto
moreover from calculation
have "q forces⇩a (π = σ)" if "q∈ℙ" "q≼p" for q
using that strengthening_eq by blast
moreover
note ‹⟨σ,r⟩∈τ› ‹r∈G›
ultimately
have "r∈ℙ ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩a (π = σ)" if "q∈ℙ" "q≼p" for q
using that leq_transD[of _ p r] by blast
then
have "dense_below({q∈ℙ. ∃s r. r∈ℙ ∧ ⟨s,r⟩ ∈ τ ∧ q≼r ∧ q forces⇩a (π = s)},p)"
using refl_leq by blast
moreover
note ‹p∈G›
moreover from calculation
have "p forces⇩a (π ∈ τ)"
using forces_mem_iff_dense_below by blast
ultimately
show ?thesis by blast
qed
end
context forcing_data1
begin
lemma Collect_forces_eq_in_M:
assumes "τ ∈ M" "θ ∈ M"
shows "{p∈ℙ. p forces⇩a (τ = θ)} ∈ M"
using assms Collect_in_M[of "forces_eq_fm(1,2,0,3,4)" "[ℙ,leq,τ,θ]"]
arity_forces_eq_fm sats_forces_eq_fm forces_eq_abs forces_eq_fm_type
by (simp add: union_abs1 Un_commute)
lemma IV240b_eq_Collects:
assumes "τ ∈ M" "θ ∈ M"
shows "{p∈ℙ. ∃σ∈domain(τ) ∪ domain(θ). p forces⇩a (σ ∈ τ) ∧ p forces⇩a (σ ∉ θ)}∈M" and
"{p∈ℙ. ∃σ∈domain(τ) ∪ domain(θ). p forces⇩a (σ ∉ τ) ∧ p forces⇩a (σ ∈ θ)}∈M"
proof -
let ?rel_pred="λM x a1 a2 a3 a4.
∃σ[M]. ∃u[M]. ∃da3[M]. ∃da4[M]. is_domain(M,a3,da3) ∧ is_domain(M,a4,da4) ∧
union(M,da3,da4,u) ∧ σ∈u ∧ is_forces_mem'(M,a1,a2,x,σ,a3) ∧
is_forces_nmem'(M,a1,a2,x,σ,a4)"
let ?φ="Exists(Exists(Exists(Exists(And(domain_fm(7,1),And(domain_fm(8,0),
And(union_fm(1,0,2),And(Member(3,2),And(forces_mem_fm(5,6,4,3,7),
forces_nmem_fm(5,6,4,3,8))))))))))"
have 1:"σ∈M" if "⟨σ,y⟩∈δ" "δ∈M" for σ δ y
using that pair_in_M_iff transitivity[of "⟨σ,y⟩" δ] by simp
have abs1:"?rel_pred(##M,p,ℙ,leq,τ,θ) ⟷
(∃σ∈domain(τ) ∪ domain(θ). forces_mem'(ℙ,leq,p,σ,τ) ∧ forces_nmem'(ℙ,leq,p,σ,θ))"
if "p∈M" for p
unfolding forces_mem_def forces_nmem_def
using assms that forces_mem'_abs forces_nmem'_abs
domain_closed Un_closed
by (auto simp add:1[of _ _ τ] 1[of _ _ θ])
have abs2:"?rel_pred(##M,p,ℙ,leq,θ,τ) ⟷ (∃σ∈domain(τ) ∪ domain(θ).
forces_nmem'(ℙ,leq,p,σ,τ) ∧ forces_mem'(ℙ,leq,p,σ,θ))" if "p∈M" for p
unfolding forces_mem_def forces_nmem_def
using assms that forces_mem'_abs forces_nmem'_abs
domain_closed Un_closed
by (auto simp add:1[of _ _ τ] 1[of _ _ θ])
have fsats1:"(M,[p,ℙ,leq,τ,θ] ⊨ ?φ) ⟷ ?rel_pred(##M,p,ℙ,leq,τ,θ)" if "p∈M" for p
using that assms sats_forces_mem_fm sats_forces_nmem_fm zero_in_M
domain_closed Un_closed by simp
have fsats2:"(M,[p,ℙ,leq,θ,τ] ⊨ ?φ) ⟷ ?rel_pred(##M,p,ℙ,leq,θ,τ)" if "p∈M" for p
using that assms sats_forces_mem_fm sats_forces_nmem_fm zero_in_M
domain_closed Un_closed by simp
have fty:"?φ∈formula" by simp
have farit:"arity(?φ)=5"
by (simp add:ord_simp_union arity)
show
"{p ∈ ℙ . ∃σ∈domain(τ) ∪ domain(θ). p forces⇩a (σ ∈ τ) ∧ p forces⇩a (σ ∉ θ)} ∈ M"
and "{p ∈ ℙ . ∃σ∈domain(τ) ∪ domain(θ). p forces⇩a (σ ∉ τ) ∧ p forces⇩a (σ ∈ θ)} ∈ M"
unfolding forces_mem_def
using abs1 fty fsats1 farit assms forces_nmem
Collect_in_M[of ?φ "[ℙ,leq,τ,θ]"]
using abs2 fty fsats2 farit assms forces_nmem domain_closed Un_closed
Collect_in_M[of ?φ "[ℙ,leq,θ,τ]"]
by simp_all
qed
end
context G_generic1
begin
lemma IV240b_eq:
includes some_rules
assumes
"val(G,τ) = val(G,θ)" "τ∈M" "θ∈M"
and
IH:"⋀σ. σ∈domain(τ)∪domain(θ) ⟹
(val(G,σ)∈val(G,τ) ⟶ (∃q∈G. q forces⇩a (σ ∈ τ))) ∧
(val(G,σ)∈val(G,θ) ⟶ (∃q∈G. q forces⇩a (σ ∈ θ)))"
shows
"∃p∈G. p forces⇩a (τ = θ)"
proof -
let ?D1="{p∈ℙ. p forces⇩a (τ = θ)}"
let ?D2="{p∈ℙ. ∃σ∈domain(τ) ∪ domain(θ). p forces⇩a (σ ∈ τ) ∧ p forces⇩a (σ ∉ θ)}"
let ?D3="{p∈ℙ. ∃σ∈domain(τ) ∪ domain(θ). p forces⇩a (σ ∉ τ) ∧ p forces⇩a (σ ∈ θ)}"
let ?D="?D1 ∪ ?D2 ∪ ?D3"
note assms
moreover from this
have "domain(τ) ∪ domain(θ)∈M" (is "?B∈M") using domain_closed Un_closed by auto
moreover from calculation
have "?D2∈M" and "?D3∈M" using IV240b_eq_Collects by simp_all
ultimately
have "?D∈M" using Collect_forces_eq_in_M Un_closed by auto
moreover
have "dense(?D)"
proof
fix p
assume "p∈ℙ"
have "∃d∈ℙ. (d forces⇩a (τ = θ) ∨
(∃σ∈domain(τ) ∪ domain(θ). d forces⇩a (σ ∈ τ) ∧ d forces⇩a (σ ∉ θ)) ∨
(∃σ∈domain(τ) ∪ domain(θ). d forces⇩a (σ ∉ τ) ∧ d forces⇩a (σ ∈ θ))) ∧
d ≼ p"
proof (cases "p forces⇩a (τ = θ)")
case True
with ‹p∈ℙ›
show ?thesis using refl_leq by blast
next
case False
moreover note ‹p∈ℙ›
moreover from calculation
obtain σ q where "σ∈domain(τ)∪domain(θ)" "q∈ℙ" "q≼p"
"(q forces⇩a (σ ∈ τ) ∧ ¬ q forces⇩a (σ ∈ θ)) ∨
(¬ q forces⇩a (σ ∈ τ) ∧ q forces⇩a (σ ∈ θ))"
using def_forces_eq by blast
moreover from this
obtain r where "r≼q" "r∈ℙ"
"(r forces⇩a (σ ∈ τ) ∧ r forces⇩a (σ ∉ θ)) ∨
(r forces⇩a (σ ∉ τ) ∧ r forces⇩a (σ ∈ θ))"
using not_forces_nmem strengthening_mem by blast
ultimately
show ?thesis using leq_transD by blast
qed
then
show "∃d∈?D . d ≼ p" by blast
qed
moreover
have "?D ⊆ ℙ"
by auto
ultimately
obtain p where "p∈G" "p∈?D"
using M_generic_denseD[of ?D] by blast
then
consider
(1) "p forces⇩a (τ = θ)" |
(2) "∃σ∈domain(τ) ∪ domain(θ). p forces⇩a (σ ∈ τ) ∧ p forces⇩a (σ ∉ θ)" |
(3) "∃σ∈domain(τ) ∪ domain(θ). p forces⇩a (σ ∉ τ) ∧ p forces⇩a (σ ∈ θ)"
by blast
then
show ?thesis
proof (cases)
case 1
with ‹p∈G›
show ?thesis by blast
next
case 2
then
obtain σ where "σ∈domain(τ) ∪ domain(θ)" "p forces⇩a (σ ∈ τ)" "p forces⇩a (σ ∉ θ)"
by blast
moreover from this and ‹p∈G› and assms
have "val(G,σ)∈val(G,τ)"
using IV240a[of σ τ] transitivity[OF _ domain_closed[simplified]] by force
moreover note ‹val(G,τ) = _›
ultimately
obtain q where "q∈G" "q forces⇩a (σ ∈ θ)"
using IH[OF ‹σ∈_›]
by auto
moreover from this and ‹p∈G›
obtain r where "r∈ℙ" "r≼p" "r≼q"
by blast
ultimately
have "r forces⇩a (σ ∈ θ)"
using strengthening_mem by blast
with ‹r≼p› ‹p forces⇩a (σ ∉ θ)› ‹r∈ℙ›
have "False"
unfolding forces_nmem_def by blast
then
show ?thesis by simp
next
case 3
then
obtain σ where "σ∈domain(τ) ∪ domain(θ)" "p forces⇩a (σ ∈ θ)" "p forces⇩a (σ ∉ τ)"
by blast
moreover from this and ‹p∈G› and assms
have "val(G,σ)∈val(G,θ)"
using IV240a[of σ θ] transitivity[OF _ domain_closed[simplified]] by force
moreover note ‹val(G,τ) = _›
ultimately
obtain q where "q∈G" "q forces⇩a (σ ∈ τ)"
using IH[OF ‹σ∈_›]
by auto
moreover from this and ‹p∈G›
obtain r where "r∈ℙ" "r≼p" "r≼q"
by blast
ultimately
have "r forces⇩a (σ ∈ τ)"
using strengthening_mem by blast
with ‹r≼p› ‹p forces⇩a (σ ∉ τ)› ‹r∈ℙ›
have "False"
unfolding forces_nmem_def by blast
then
show ?thesis by simp
qed
qed
lemma IV240b:
"(τ∈M⟶θ∈M⟶val(G,τ) = val(G,θ) ⟶ (∃p∈G. p forces⇩a (τ = θ))) ∧
(τ∈M⟶θ∈M⟶val(G,τ) ∈ val(G,θ) ⟶ (∃p∈G. p forces⇩a (τ ∈ θ)))"
(is "?Q(τ,θ) ∧ ?R(τ,θ)")
proof (intro forces_induction)
fix τ θ p
assume "σ∈domain(θ) ⟹ ?Q(τ, σ)" for σ
then show "?R(τ, θ)"
using IV240b_mem domain_closed transitivity by simp
next
fix τ θ p
assume "σ ∈ domain(τ) ∪ domain(θ) ⟹ ?R(σ,τ) ∧ ?R(σ,θ)" for σ
moreover from this
have IH':"τ∈M ⟹ θ∈M ⟹ σ ∈ domain(τ) ∪ domain(θ) ⟹
(val(G, σ) ∈ val(G, τ) ⟶ (∃q∈G. q forces⇩a (σ ∈ τ))) ∧
(val(G, σ) ∈ val(G, θ) ⟶ (∃q∈G. q forces⇩a (σ ∈ θ)))" for σ
using domain_trans[OF trans_M]
by blast
ultimately
show "?Q(τ,θ)"
using IV240b_eq by auto
qed
lemma truth_lemma_mem:
assumes
"env∈list(M)"
"n∈nat" "m∈nat" "n<length(env)" "m<length(env)"
shows
"(∃p∈G. p ⊩ Member(n,m) env) ⟷ M[G], map(val(G),env) ⊨ Member(n,m)"
using assms IV240a[of "nth(n,env)" "nth(m,env)"]
IV240b[of "nth(n,env)" "nth(m,env)"]
M_genericD
Forces_Member[of _ "nth(n,env)" "nth(m,env)" env n m] map_val_in_MG
by auto
lemma truth_lemma_eq:
assumes
"env∈list(M)"
"n∈nat" "m∈nat" "n<length(env)" "m<length(env)"
shows
"(∃p∈G. p ⊩ Equal(n,m) env) ⟷ M[G], map(val(G),env) ⊨ Equal(n,m)"
using assms IV240a(1)[of "nth(n,env)" "nth(m,env)"]
IV240b(1)[of "nth(n,env)" "nth(m,env)"]
M_genericD
Forces_Equal[of _ "nth(n,env)" "nth(m,env)" env n m] map_val_in_MG
by auto
end
lemma arities_at_aux:
assumes
"n ∈ nat" "m ∈ nat" "env ∈ list(M)" "succ(n) ∪ succ(m) ≤ length(env)"
shows
"n < length(env)" "m < length(env)"
using assms succ_leE[OF Un_leD1, of n "succ(m)" "length(env)"]
succ_leE[OF Un_leD2, of "succ(n)" m "length(env)"] by auto
subsection‹The Strenghtening Lemma›
context forcing_data1
begin
lemma strengthening_lemma:
assumes
"p∈ℙ" "φ∈formula" "r∈ℙ" "r≼p"
"env∈list(M)" "arity(φ)≤length(env)"
shows
"p ⊩ φ env ⟹ r ⊩ φ env"
using assms(2-)
proof (induct arbitrary:env)
case (Member n m)
then
have "n<length(env)" "m<length(env)"
using arities_at_aux by simp_all
moreover
assume "env∈list(M)"
moreover
note assms Member
ultimately
show ?case
using Forces_Member[of _ "nth(n,env)" "nth(m,env)" env n m]
strengthening_mem[of p r "nth(n,env)" "nth(m,env)"] by simp
next
case (Equal n m)
then
have "n<length(env)" "m<length(env)"
using arities_at_aux by simp_all
moreover
assume "env∈list(M)"
moreover
note assms Equal
ultimately
show ?case
using Forces_Equal[of _ "nth(n,env)" "nth(m,env)" env n m]
strengthening_eq[of p r "nth(n,env)" "nth(m,env)"] by simp
next
case (Nand φ ψ)
with assms
show ?case
using Forces_Nand transitivity[OF _ P_in_M] pair_in_M_iff
transitivity[OF _ leq_in_M] leq_transD by auto
next
case (Forall φ)
with assms
have "p ⊩ φ ([x] @ env)" if "x∈M" for x
using that Forces_Forall by simp
with Forall
have "r ⊩ φ ([x] @ env)" if "x∈M" for x
using that pred_le2 by (simp)
with assms Forall
show ?case
using Forces_Forall by simp
qed
subsection‹The Density Lemma›
lemma arity_Nand_le:
assumes "φ ∈ formula" "ψ ∈ formula" "arity(Nand(φ, ψ)) ≤ length(env)" "env∈list(A)"
shows "arity(φ) ≤ length(env)" "arity(ψ) ≤ length(env)"
using assms
by (rule_tac Un_leD1, rule_tac [5] Un_leD2, auto)
lemma dense_below_imp_forces:
assumes
"p∈ℙ" "φ∈formula"
"env∈list(M)" "arity(φ)≤length(env)"
shows
"dense_below({q∈ℙ. (q ⊩ φ env)},p) ⟹ (p ⊩ φ env)"
using assms(2-)
proof (induct arbitrary:env)
case (Member n m)
then
have "n<length(env)" "m<length(env)"
using arities_at_aux by simp_all
moreover
assume "env∈list(M)"
moreover
note assms Member
ultimately
show ?case
using Forces_Member[of _ "nth(n,env)" "nth(m,env)" env n m]
density_mem[of p "nth(n,env)" "nth(m,env)"] by simp
next
case (Equal n m)
then
have "n<length(env)" "m<length(env)"
using arities_at_aux by simp_all
moreover
assume "env∈list(M)"
moreover
note assms Equal
ultimately
show ?case
using Forces_Equal[of _ "nth(n,env)" "nth(m,env)" env n m]
density_eq[of p "nth(n,env)" "nth(m,env)"] by simp
next
case (Nand φ ψ)
{
fix q
assume "q∈M" "q∈ℙ" "q≼ p" "q ⊩ φ env"
moreover
note Nand
moreover from calculation
obtain d where "d∈ℙ" "d ⊩ Nand(φ, ψ) env" "d≼ q"
using dense_belowI by auto
moreover from calculation
have "¬(d⊩ ψ env)" if "d ⊩ φ env"
using that Forces_Nand refl_leq transitivity[OF _ P_in_M, of d] by auto
moreover
note arity_Nand_le[of φ ψ]
moreover from calculation
have "d ⊩ φ env"
using strengthening_lemma[of q φ d env] Un_leD1 by auto
ultimately
have "¬ (q ⊩ ψ env)"
using strengthening_lemma[of q ψ d env] by auto
}
with ‹p∈ℙ›
show ?case
using Forces_Nand[symmetric, OF _ Nand(6,1,3)] by blast
next
case (Forall φ)
have "dense_below({q∈ℙ. q ⊩ φ ([a]@env)},p)" if "a∈M" for a
proof
fix r
assume "r∈ℙ" "r≼p"
with ‹dense_below(_,p)›
obtain q where "q∈ℙ" "q≼r" "q ⊩ Forall(φ) env"
by blast
moreover
note Forall ‹a∈M›
moreover from calculation
have "q ⊩ φ ([a]@env)"
using Forces_Forall by simp
ultimately
show "∃d ∈ {q∈ℙ. q ⊩ φ ([a]@env)}. d ∈ ℙ ∧ d≼r"
by auto
qed
moreover
note Forall(2)[of "Cons(_,env)"] Forall(1,3-5)
ultimately
have "p ⊩ φ ([a]@env)" if "a∈M" for a
using that pred_le2 by simp
with assms Forall
show ?case using Forces_Forall by simp
qed
lemma density_lemma:
assumes
"p∈ℙ" "φ∈formula" "env∈list(M)" "arity(φ)≤length(env)"
shows
"p ⊩ φ env ⟷ dense_below({q∈ℙ. (q ⊩ φ env)},p)"
proof
assume "dense_below({q∈ℙ. (q ⊩ φ env)},p)"
with assms
show "(p ⊩ φ env)"
using dense_below_imp_forces by simp
next
assume "p ⊩ φ env"
with assms
show "dense_below({q∈ℙ. q ⊩ φ env},p)"
using strengthening_lemma refl_leq by auto
qed
subsection‹The Truth Lemma›
lemma Forces_And:
assumes
"p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula"
"arity(φ) ≤ length(env)" "arity(ψ) ≤ length(env)"
shows
"p ⊩ And(φ,ψ) env ⟷ (p ⊩ φ env) ∧ (p ⊩ ψ env)"
proof
assume "p ⊩ And(φ, ψ) env"
with assms
have "dense_below({r ∈ ℙ . (r ⊩ φ env) ∧ (r ⊩ ψ env)}, p)"
using Forces_And_iff_dense_below by simp
then
have "dense_below({r ∈ ℙ . (r ⊩ φ env)}, p)" "dense_below({r ∈ ℙ . (r ⊩ ψ env)}, p)"
by blast+
with assms
show "(p ⊩ φ env) ∧ (p ⊩ ψ env)"
using density_lemma[symmetric] by simp
next
assume "(p ⊩ φ env) ∧ (p ⊩ ψ env)"
have "dense_below({r ∈ ℙ . (r ⊩ φ env) ∧ (r ⊩ ψ env)}, p)"
proof (intro dense_belowI bexI conjI, assumption)
fix q
assume "q∈ℙ" "q≼ p"
with assms ‹(p ⊩ φ env) ∧ (p ⊩ ψ env)›
show "q∈{r ∈ ℙ . (r ⊩ φ env) ∧ (r ⊩ ψ env)}" "q≼ q"
using strengthening_lemma refl_leq by auto
qed
with assms
show "p ⊩ And(φ,ψ) env"
using Forces_And_iff_dense_below by simp
qed
lemma Forces_Nand_alt:
assumes
"p∈ℙ" "env ∈ list(M)" "φ∈formula" "ψ∈formula"
"arity(φ) ≤ length(env)" "arity(ψ) ≤ length(env)"
shows
"(p ⊩ Nand(φ,ψ) env) ⟷ (p ⊩ Neg(And(φ,ψ)) env)"
using assms Forces_Nand Forces_And Forces_Neg by auto
end
context G_generic1
begin
lemma truth_lemma_Neg:
assumes
"φ∈formula" "env∈list(M)" "arity(φ)≤length(env)" and
IH: "(∃p∈G. p ⊩ φ env) ⟷ M[G], map(val(G),env) ⊨ φ"
shows
"(∃p∈G. p ⊩ Neg(φ) env) ⟷ M[G], map(val(G),env) ⊨ Neg(φ)"
proof (intro iffI, elim bexE, rule ccontr)
fix p
assume "p∈G" "p ⊩ Neg(φ) env" "¬(M[G],map(val(G),env) ⊨ Neg(φ))"
moreover
note assms
moreover from calculation
have "M[G], map(val(G),env) ⊨ φ" "p∈ℙ"
using map_val_in_MG by auto
with IH
obtain r where "r ⊩ φ env" "r∈G" "r∈ℙ" by blast
moreover from this and ‹p∈G›
obtain q where "q≼p" "q≼r" "q∈G" "q∈ℙ" "q∈M"
using transitivity[OF _ P_in_M]
by blast
moreover from calculation
have "q ⊩ φ env"
using strengthening_lemma
by simp
with assms ‹p ⊩ _ _› ‹q≼p› ‹q∈M› ‹p∈ℙ› ‹q∈ℙ›
show "False"
using Forces_Neg
by auto
next
assume "M[G], map(val(G),env) ⊨ Neg(φ)"
with assms
have "¬ (M[G], map(val(G),env) ⊨ φ)"
using map_val_in_MG by simp
let ?D="{p∈ℙ. (p ⊩ φ env) ∨ (p ⊩ Neg(φ) env)}"
from assms
have "?D ∈ M"
using separation_disj separation_closed separation_forces by simp
moreover
have "?D ⊆ ℙ" by auto
moreover
have "dense(?D)"
proof
fix q
assume "q∈ℙ"
with assms
show "∃d∈{p ∈ ℙ . (p ⊩ φ env) ∨ (p ⊩ Neg(φ) env)}. d≼ q"
using refl_leq Forces_Neg by (cases "q ⊩ Neg(φ) env", auto)
qed
ultimately
obtain p where "p∈G" "(p ⊩ φ env) ∨ (p ⊩ Neg(φ) env)"
by blast
then
consider (1) "p ⊩ φ env" | (2) "p ⊩ Neg(φ) env" by blast
then
show "∃p∈G. (p ⊩ Neg(φ) env)"
proof (cases)
case 1
with ‹¬ (M[G],map(val(G),env) ⊨ φ)› ‹p∈G› IH
show ?thesis
by blast
next
case 2
with ‹p∈G›
show ?thesis by blast
qed
qed
lemma truth_lemma_And:
assumes
"env∈list(M)" "φ∈formula" "ψ∈formula"
"arity(φ)≤length(env)" "arity(ψ) ≤ length(env)"
and
IH: "(∃p∈G. p ⊩ φ env) ⟷ M[G], map(val(G),env) ⊨ φ"
"(∃p∈G. p ⊩ ψ env) ⟷ M[G], map(val(G),env) ⊨ ψ"
shows
"(∃p∈G. (p ⊩ And(φ,ψ) env)) ⟷ M[G] , map(val(G),env) ⊨ And(φ,ψ)"
using assms map_val_in_MG Forces_And[OF M_genericD assms(1-5)]
proof (intro iffI, elim bexE)
fix p
assume "p∈G" "p ⊩ And(φ,ψ) env"
with assms
show "M[G], map(val(G),env) ⊨ And(φ,ψ)"
using Forces_And[of _ _ φ ψ] map_val_in_MG M_genericD by auto
next
assume "M[G], map(val(G),env) ⊨ And(φ,ψ)"
moreover
note assms
moreover from calculation
obtain q r where "q ⊩ φ env" "r ⊩ ψ env" "q∈G" "r∈G" "r∈ℙ" "q∈ℙ"
using map_val_in_MG Forces_And[OF M_genericD assms(1-5)] M_genericD by auto
moreover from calculation
obtain p where "p≼q" "p≼r" "p∈G"
by auto
moreover from calculation
have "(p ⊩ φ env) ∧ (p ⊩ ψ env)"
using strengthening_lemma[OF M_genericD] by force
ultimately
show "∃p∈G. (p ⊩ And(φ,ψ) env)"
using Forces_And[OF M_genericD assms(1-5)] by auto
qed
end
definition
ren_truth_lemma :: "i⇒i" where
"ren_truth_lemma(φ) ≡
Exists(Exists(Exists(Exists(Exists(
And(Equal(0,5),And(Equal(1,8),And(Equal(2,9),And(Equal(3,10),And(Equal(4,6),
iterates(λp. incr_bv(p)`5 , 6, φ)))))))))))"
lemma ren_truth_lemma_type[TC] :
"φ∈formula ⟹ ren_truth_lemma(φ) ∈formula"
unfolding ren_truth_lemma_def
by simp
lemma arity_ren_truth :
assumes "φ∈formula"
shows "arity(ren_truth_lemma(φ)) ≤ 6 ∪ succ(arity(φ))"
proof -
consider (lt) "5 <arity(φ)" | (ge) "¬ 5 < arity(φ)"
by auto
then
show ?thesis
proof cases
case lt
consider (a) "5<arity(φ)+⇩ω5" | (b) "arity(φ)+⇩ω5 ≤ 5"
using not_lt_iff_le ‹φ∈_› by force
then
show ?thesis
proof cases
case a
with ‹φ∈_› lt
have "5 < succ(arity(φ))" "5<arity(φ)+⇩ω2" "5<arity(φ)+⇩ω3" "5<arity(φ)+⇩ω4"
using succ_ltI by auto
with ‹φ∈_›
have c:"arity(iterates(λp. incr_bv(p)`5,5,φ)) = 5+⇩ωarity(φ)" (is "arity(?φ') = _")
using arity_incr_bv_lemma lt a
by simp
with ‹φ∈_›
have "arity(incr_bv(?φ')`5) = 6+⇩ωarity(φ)"
using arity_incr_bv_lemma[of ?φ' 5] a by auto
with ‹φ∈_›
show ?thesis
unfolding ren_truth_lemma_def
using pred_Un_distrib union_abs1 Un_assoc[symmetric] a c union_abs2
by (simp add:arity)
next
case b
with ‹φ∈_› lt
have "5 < succ(arity(φ))" "5<arity(φ)+⇩ω2" "5<arity(φ)+⇩ω3" "5<arity(φ)+⇩ω4" "5<arity(φ)+⇩ω5"
using succ_ltI by auto
with ‹φ∈_›
have "arity(iterates(λp. incr_bv(p)`5,6,φ)) = 6+⇩ωarity(φ)" (is "arity(?φ') = _")
using arity_incr_bv_lemma lt
by simp
with ‹φ∈_›
show ?thesis
unfolding ren_truth_lemma_def
using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2
by (simp add:arity)
qed
next
case ge
with ‹φ∈_›
have "arity(φ) ≤ 5" "pred^5(arity(φ)) ≤ 5"
using not_lt_iff_le le_trans[OF le_pred]
by auto
with ‹φ∈_›
have "arity(iterates(λp. incr_bv(p)`5,6,φ)) = arity(φ)" "arity(φ)≤6" "pred^5(arity(φ)) ≤ 6"
using arity_incr_bv_lemma ge le_trans[OF ‹arity(φ)≤5›] le_trans[OF ‹pred^5(arity(φ))≤5›]
by auto
with ‹arity(φ) ≤ 5› ‹φ∈_› ‹pred^5(_) ≤ 5›
show ?thesis
unfolding ren_truth_lemma_def
using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2
by (simp add:arity)
qed
qed
lemma sats_ren_truth_lemma:
"[q,b,d,a1,a2,a3] @ env ∈ list(M) ⟹ φ ∈ formula ⟹
(M, [q,b,d,a1,a2,a3] @ env ⊨ ren_truth_lemma(φ) ) ⟷
(M, [q,a1,a2,a3,b] @ env ⊨ φ)"
unfolding ren_truth_lemma_def
by (insert sats_incr_bv_iff [of _ _ M _ "[q,a1,a2,a3,b]"], simp)
context forcing_data1
begin
lemma truth_lemma' :
assumes
"φ∈formula" "env∈list(M)" "arity(φ) ≤ succ(length(env))"
shows
"separation(##M,λd. ∃b∈M. ∀q∈ℙ. q≼d ⟶ ¬(q ⊩ φ ([b]@env)))"
proof -
let ?rel_pred="λM x a1 a2 a3. ∃b∈M. ∀q∈M. q∈a1 ∧ is_leq(##M,a2,q,x) ⟶
¬(M, [q,a1,a2,a3,b] @ env ⊨ forces(φ))"
let ?ψ="Exists(Forall(Implies(And(Member(0,3),is_leq_fm(4,0,2)),
Neg(ren_truth_lemma(forces(φ))))))"
have "q∈M" if "q∈ℙ" for q using that transitivity[OF _ P_in_M] by simp
then
have 1:"∀q∈M. q∈ℙ ∧ R(q) ⟶ Q(q) ⟹ (∀q∈ℙ. R(q) ⟶ Q(q))" for R Q
by auto
then
have "⟦b ∈ M; ∀q∈M. q ∈ ℙ ∧ q ≼ d ⟶ ¬(q ⊩ φ ([b]@env))⟧ ⟹
∃c∈M. ∀q∈ℙ. q ≼ d ⟶ ¬(q ⊩ φ ([c]@env))" for b d
by (rule bexI,simp_all)
then
have "?rel_pred(M,d,ℙ,leq,𝟭) ⟷ (∃b∈M. ∀q∈ℙ. q≼d ⟶ ¬(q ⊩ φ ([b]@env)))" if "d∈M" for d
using that leq_abs assms
by auto
moreover
have "?ψ∈formula" using assms by simp
moreover
have "(M, [d,ℙ,leq,𝟭]@env ⊨ ?ψ) ⟷ ?rel_pred(M,d,ℙ,leq,𝟭)" if "d∈M" for d
using assms that sats_is_leq_fm sats_ren_truth_lemma zero_in_M
by simp
moreover
have "arity(?ψ) ≤ 4+⇩ωlength(env)"
proof -
have eq:"arity(is_leq_fm(4, 0, 2)) = 5"
using arity_is_leq_fm succ_Un_distrib ord_simp_union
by simp
with ‹φ∈_›
have "arity(?ψ) = 3 ∪ (pred^2(arity(ren_truth_lemma(forces(φ)))))"
using union_abs1 pred_Un_distrib by (simp add:arity)
moreover
have "... ≤ 3 ∪ (pred(pred(6 ∪ succ(arity(forces(φ))))))" (is "_ ≤ ?r")
using ‹φ∈_› Un_le_compat[OF le_refl[of 3]]
le_imp_subset arity_ren_truth[of "forces(φ)"]
pred_mono
by auto
finally
have "arity(?ψ) ≤ ?r" by simp
have i:"?r ≤ 4 ∪ pred(arity(forces(φ)))"
using pred_Un_distrib pred_succ_eq ‹φ∈_› Un_assoc[symmetric] union_abs1 by simp
have h:"4 ∪ pred(arity(forces(φ))) ≤ 4 ∪ (4+⇩ωlength(env))"
using ‹env∈_› add_commute ‹φ∈_›
Un_le_compat[of 4 4,OF _ pred_mono[OF _ arity_forces_le[OF _ _ ‹arity(φ)≤_›]] ]
‹env∈_› by auto
with ‹φ∈_› ‹env∈_›
show ?thesis
using le_trans[OF ‹arity(?ψ) ≤ ?r› le_trans[OF i h]] ord_simp_union by simp
qed
ultimately
show ?thesis using assms
separation_ax[of "?ψ" "[ℙ,leq,𝟭]@env"]
separation_cong[of "##M" "λy. (M, [y,ℙ,leq,𝟭]@env ⊨?ψ)"]
by simp
qed
end
context G_generic1
begin
lemma truth_lemma:
assumes
"φ∈formula"
"env∈list(M)" "arity(φ)≤length(env)"
shows
"(∃p∈G. p ⊩ φ env) ⟷ M[G], map(val(G),env) ⊨ φ"
using assms
proof (induct arbitrary:env)
case (Member x y)
then
show ?case
using truth_lemma_mem[OF ‹env∈list(M)› ‹x∈nat› ‹y∈nat›] arities_at_aux
by simp
next
case (Equal x y)
then
show ?case
using truth_lemma_eq[OF ‹env∈list(M)› ‹x∈nat› ‹y∈nat›] arities_at_aux by simp
next
case (Nand φ ψ)
then
show ?case
using truth_lemma_And truth_lemma_Neg[of "⋅φ ∧ ψ⋅"] Forces_Nand_alt
M_genericD map_val_in_MG arity_Nand_le[of φ ψ] FOL_arities by auto
next
case (Forall φ)
then
show ?case
proof (intro iffI)
assume "∃p∈G. (p ⊩ Forall(φ) env)"
then
obtain p where "p∈G" "p∈M" "p∈ℙ" "p ⊩ Forall(φ) env"
using transitivity[OF _ P_in_M] by auto
with ‹env∈list(M)› ‹φ∈formula›
have "p ⊩ φ ([x]@env)" if "x∈M" for x
using that Forces_Forall by simp
with ‹p∈G› ‹φ∈formula› ‹env∈_› ‹arity(Forall(φ)) ≤ length(env)›
Forall(2)[of "Cons(_,env)"]
show "M[G], map(val(G),env) ⊨ Forall(φ)"
using pred_le2 map_val_in_MG
by (auto iff:GenExt_iff)
next
assume "M[G], map(val(G),env) ⊨ Forall(φ)"
let ?D1="{d∈ℙ. (d ⊩ Forall(φ) env)}"
let ?D2="{d∈ℙ. ∃b∈M. ∀q∈ℙ. q≼d ⟶ ¬(q ⊩ φ ([b]@env))}"
define D where "D ≡ ?D1 ∪ ?D2"
note ‹arity(Forall(φ)) ≤ length(env)› ‹φ∈formula› ‹env∈list(M)›
moreover from this
have arφ:"arity(φ)≤succ(length(env))"
using pred_le2 by simp
moreover from calculation
have "?D1∈M" using Collect_forces by simp
moreover from ‹env∈list(M)› ‹φ∈formula›
have "?D2∈M"
using truth_lemma'[of φ] separation_closed arφ
by simp
ultimately
have "D∈M" unfolding D_def using Un_closed by simp
moreover
have "D ⊆ ℙ" unfolding D_def by auto
moreover
have "dense(D)"
proof
fix p
assume "p∈ℙ"
show "∃d∈D. d≼ p"
proof (cases "p ⊩ Forall(φ) env")
case True
with ‹p∈ℙ›
show ?thesis unfolding D_def using refl_leq by blast
next
case False
with Forall ‹p∈ℙ›
obtain b where "b∈M" "¬(p ⊩ φ ([b]@env))"
using Forces_Forall by blast
moreover from this ‹p∈ℙ› Forall
have "¬dense_below({q∈ℙ. q ⊩ φ ([b]@env)},p)"
using density_lemma pred_le2 by auto
moreover from this
obtain d where "d≼p" "∀q∈ℙ. q≼d ⟶ ¬(q ⊩ φ ([b] @ env))"
"d∈ℙ" by blast
ultimately
show ?thesis unfolding D_def by auto
qed
qed
moreover
note generic
ultimately
obtain d where "d ∈ D" "d ∈ G" by blast
then
consider (1) "d∈?D1" | (2) "d∈?D2" unfolding D_def by blast
then
show "∃p∈G. (p ⊩ Forall(φ) env)"
proof (cases)
case 1
with ‹d∈G›
show ?thesis by blast
next
case 2
then
obtain b where "b∈M" "∀q∈ℙ. q≼d ⟶¬(q ⊩ φ ([b] @ env))"
by blast
moreover from this(1) and ‹M[G], _ ⊨ Forall(φ)› and
Forall(2)[of "Cons(b,env)"] Forall(1,3-)
obtain p where "p∈G" "p∈ℙ" "p ⊩ φ ([b] @ env)"
using pred_le2 map_val_in_MG M_genericD by (auto iff:GenExt_iff)
moreover
note ‹d∈G›
ultimately
obtain q where "q∈G" "q∈ℙ" "q≼d" "q≼p"
using M_genericD by force
moreover from this and ‹p ⊩ φ ([b] @ env)›
Forall ‹b∈M› ‹p∈ℙ›
have "q ⊩ φ ([b] @ env)"
using pred_le2 strengthening_lemma by simp
moreover
note ‹∀q∈ℙ. q≼d ⟶¬(q ⊩ φ ([b] @ env))›
ultimately
show ?thesis by simp
qed
qed
qed
end
context forcing_data1
begin
subsection‹The ``Definition of forcing''›
lemma definition_of_forcing:
assumes
"p∈ℙ" "φ∈formula" "env∈list(M)" "arity(φ)≤length(env)"
shows
"(p ⊩ φ env) ⟷
(∀G. M_generic(G) ∧ p∈G ⟶ M[G], map(val(G),env) ⊨ φ)"
proof (intro iffI allI impI, elim conjE)
fix G
assume "(p ⊩ φ env)" "M_generic(G)" "p ∈ G"
moreover from this
interpret G_generic1 ℙ leq 𝟭 M enum G
by (unfold_locales,simp)
from calculation assms
show "M[G], map(val(G),env) ⊨ φ"
using truth_lemma[of φ] by auto
next
assume 1: "∀G.(M_generic(G)∧ p∈G) ⟶ M[G] , map(val(G),env) ⊨ φ"
{
fix r
assume 2: "r∈ℙ" "r≼p"
then
obtain G where "r∈G" "M_generic(G)"
text‹Here we're using countability (via the existence of
generic filters) of \<^term>‹M› as a shortcut.›
using generic_filter_existence by auto
moreover from this
interpret G_generic1 ℙ leq 𝟭 M enum G
by (unfold_locales,simp)
from calculation 2 ‹p∈ℙ›
have "p∈G"
using filter_leqD by auto
moreover note 1
ultimately
have "M[G], map(val(G),env) ⊨ φ"
by simp
moreover
note assms
moreover from calculation
obtain s where "s∈G" "(s ⊩ φ env)"
using truth_lemma[of φ] by blast
moreover from this ‹r∈G›
obtain q where "q∈G" "q≼s" "q≼r" "s∈ℙ" "q∈ℙ"
by blast
ultimately
have "∃q∈ℙ. q≼r ∧ (q ⊩ φ env)"
using strengthening_lemma[of s] by auto
}
then
have "dense_below({q∈ℙ. (q ⊩ φ env)},p)"
unfolding dense_below_def by blast
with assms
show "(p ⊩ φ env)"
using density_lemma by blast
qed
lemmas definability = forces_type
end
end