Theory Definitions_Main

section‹Main definitions of the development›

theory Definitions_Main
  imports Forcing_Main

begin

text‹This theory gathers the main definitions of the Forcing session.

It might be considered as the bare minimum reading requisite to
trust that our development indeed formalizes the theory of
forcing. This should be mathematically clear since this is the
only known method for obtaining proper extensions of ctms while
preserving the ordinals.

The main theorem of this session and all of its relevant definitions
appear in Section~\ref{sec:def-main-forcing}. The reader trusting
all the libraries in which our development is based, might jump
directly there. But in case one wants to dive deeper, the following
sections treat some basic concepts in the ZF logic
(Section~\ref{sec:def-main-ZF})  and in the
ZF-Constructible library (Section~\ref{sec:def-main-constructible})
on which our definitions are built.
›

declare [[show_question_marks=false]]

subsection‹ZF\label{sec:def-main-ZF}›

text‹For the basic logic ZF we restrict ourselves to just a few
concepts.›

thm bij_def[unfolded inj_def surj_def]
text‹@{thm [display] bij_def[unfolded inj_def surj_def]}›
(*
  bij(A, B) ≡ {f ∈ A → B . ∀w∈A. ∀x∈A. f ` w = f ` x ⟶ w = x}
               ∩ {f ∈ A → B . ∀y∈B. ∃x∈A. f ` x = y}
*)

thm eqpoll_def
text‹@{thm [display] eqpoll_def}›
(*
  A ≈ B ≡ ∃f. f ∈ bij(A, B)
*)

thm Transset_def
text‹@{thm [display] Transset_def}›
(*
  Transset(i) ≡ ∀x∈i. x ⊆ i
*)

thm Ord_def
text‹@{thm [display] Ord_def}›
(*
  Ord(i) ≡ Transset(i) ∧ (∀x∈i. Transset(x))
*)

thm lt_def
text‹@{thm [display] lt_def}›
(*
  i < j ≡ i ∈ j ∧ Ord(j)
*)

text‹The set of natural numbers \<^term>‹ω› is defined as a
fixpoint, but here we just write its characterization as the
first limit ordinal.›
thm Limit_nat[unfolded Limit_def] nat_le_Limit[unfolded Limit_def]
text‹@{thm [display] Limit_nat[unfolded Limit_def]
 nat_le_Limit[unfolded Limit_def]}›
(*
  Ord(ω) ∧ 0 < ω ∧ (∀y. y < ω ⟶ succ(y) < ω)
  Ord(i) ∧ 0 < i ∧ (∀y. y < i ⟶ succ(y) < i) ⟹ ω ≤ i
*)

hide_const (open) Order.pred
thm add_0_right add_succ_right pred_0 pred_succ_eq
text‹@{thm [display] add_succ_right add_0_right pred_0 pred_succ_eq}›
(*
  m ∈ ω ⟹ m #+ 0 = m
  m #+ succ(n) = succ(m #+ n)

  pred(0) = 0
  pred(succ(y)) = y
*)

text‹Lists›

thm Nil Cons list.induct
text‹@{thm [display] Nil Cons list.induct }›
(*
  [] ∈ list(A)
  a ∈ A ⟹ l ∈ list(A) ⟹ Cons(a, l) ∈ list(A)
  x ∈ list(A) ⟹ P([]) ⟹ (⋀a l. a ∈ A ⟹ l ∈ list(A) ⟹ P(l) ⟹ P(Cons(a, l))) ⟹ P(x)
*)
thm length.simps app.simps nth_0 nth_Cons
text‹@{thm [display] length.simps app.simps nth_0 nth_Cons}›
(*
  length([]) = 0
  length(Cons(a, l)) = succ(length(l))

  [] @ ys = ys
  Cons(a, l) @ ys = Cons(a, l @ ys)

  nth(0, Cons(a, l)) = a
  n ∈ ω ⟹ nth(succ(n), Cons(a, l)) = nth(n, l)
*)

txt‹Relative quantifications›

lemma "∀x[M]. P(x) ≡ ∀x. M(x) ⟶ P(x)"
      "∃x[M]. P(x) ≡ ∃x. M(x) ∧ P(x)"
  unfolding rall_def rex_def .

thm setclass_iff
text‹@{thm [display] setclass_iff}›
(*
  (##A)(x) ⟷ x ∈ A
*)

subsection‹ZF-Constructible\label{sec:def-main-constructible}›

thm big_union_def
text‹@{thm [display] big_union_def}›
(*
  big_union(M, A, z) ≡ ∀x[M]. x ∈ z ⟷ (∃y[M]. y ∈ A ∧ x ∈ y)
*)


thm Union_ax_def
text‹@{thm [display] Union_ax_def}›
(*
  Union_ax(M) ≡ ∀x[M]. ∃z[M]. ∀xa[M]. xa ∈ z ⟷ (∃y[M]. y ∈ x ∧ xa ∈ y)
*)

thm power_ax_def[unfolded powerset_def subset_def]
text‹@{thm [display] power_ax_def[unfolded powerset_def subset_def]}›
(*
  power_ax(M) ≡ ∀x[M]. ∃z[M]. ∀xa[M]. xa ∈ z ⟷ (∀xb[M]. xb ∈ xa ⟶ xb ∈ x)
*)

thm upair_def
text‹@{thm [display] upair_def}›
(*
  upair(M, a, b, z) ≡ a ∈ z ∧ b ∈ z ∧ (∀x[M]. x ∈ z ⟶ x = a ∨ x = b)
*)

thm pair_def
text‹@{thm [display] pair_def}›
(*
  pair(M, a, b, z) ≡ ∃x[M]. upair(M, a, a, x) ∧
                        (∃y[M]. upair(M, a, b, y) ∧ upair(M, x, y, z))
*)

thm successor_def[unfolded is_cons_def union_def]
text‹@{thm [display] successor_def[unfolded is_cons_def union_def]}›
(*
  successor(M, a, z) ≡ ∃x[M]. upair(M, a, a, x) ∧ (∀xa[M]. xa ∈ z ⟷ xa ∈ x ∨ xa ∈ a)
*)

thm upair_ax_def
text‹@{thm [display] upair_ax_def}›
(*
  upair_ax(M) ≡ ∀x[M]. ∀y[M]. ∃z[M]. upair(M, x, y, z)
*)

thm foundation_ax_def
text‹@{thm [display] foundation_ax_def}›
(*
  foundation_ax(M) ≡ ∀x[M]. (∃y[M]. y ∈ x) ⟶ (∃y[M]. y ∈ x ∧ ¬ (∃z[M]. z ∈ x ∧ z ∈ y))
*)

thm extensionality_def
text‹@{thm [display] extensionality_def}›
(*
  extensionality(M) ≡ ∀x[M]. ∀y[M]. (∀z[M]. z ∈ x ⟷ z ∈ y) ⟶ x = y
*)

thm separation_def
text‹@{thm [display] separation_def}›
(*
  separation(M, P) ≡ ∀z[M]. ∃y[M]. ∀x[M]. x ∈ y ⟷ x ∈ z ∧ P(x)
*)

thm univalent_def
text‹@{thm [display] univalent_def}›
(*
  univalent(M, A, P) ≡ ∀x[M]. x ∈ A ⟶
                          (∀y[M]. ∀z[M]. P(x, y) ∧ P(x, z) ⟶ y = z)
*)

thm strong_replacement_def
text‹@{thm [display] strong_replacement_def}›
(*
  strong_replacement(M, P) ≡ ∀A[M]. univalent(M, A, P) ⟶
       (∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x[M]. x ∈ A ∧ P(x, b)))
*)

thm empty_def
text‹@{thm [display] empty_def}›
(*
  empty(M, z) ≡ ∀x[M]. x ∉ z
*)

thm transitive_set_def[unfolded subset_def]
text‹@{thm [display] transitive_set_def[unfolded subset_def]}›
(*
  transitive_set(M, a) ≡ ∀x[M]. x ∈ a ⟶ (∀xa[M]. xa ∈ x ⟶ xa ∈ a)
*)


thm ordinal_def
text‹@{thm [display] ordinal_def}›
(*
  ordinal(M, a) ≡ transitive_set(M, a) ∧ (∀x[M]. x ∈ a ⟶
                                              transitive_set(M, x))
*)

thm image_def
text‹@{thm [display] image_def}›
(*
  image(M, r, A, z) ≡ ∀y[M]. y ∈ z ⟷
                (∃w[M]. w ∈ r ∧ (∃x[M]. x ∈ A ∧ pair(M, x, y, w)))
*)

thm fun_apply_def
text‹@{thm [display] fun_apply_def}›
(*
  fun_apply(M, f, x, y) ≡ ∃xs[M]. ∃fxs[M]. upair(M, x, x, xs) ∧
                       image(M, f, xs, fxs) ∧ big_union(M, fxs, y)
*)

thm is_function_def
text‹@{thm [display] is_function_def}›
(*
  is_function(M, r) ≡ ∀x[M]. ∀y[M]. ∀y'[M]. ∀p[M]. ∀p'[M].
       pair(M, x, y, p) ⟶ pair(M, x, y', p') ⟶ p ∈ r ⟶ p' ∈ r ⟶ y = y'
*)

thm is_relation_def
text‹@{thm [display] is_relation_def}›
(*
  is_relation(M, r) ≡ ∀z[M]. z ∈ r ⟶ (∃x[M]. ∃y[M]. pair(M, x, y, z))
*)

thm is_domain_def
text‹@{thm [display] is_domain_def}›
(*
  is_domain(M, r, z) ≡ ∀x[M]. x ∈ z ⟷
                        (∃w[M]. w ∈ r ∧ (∃y[M]. pair(M, x, y, w)))
*)

thm typed_function_def
text‹@{thm [display] typed_function_def}›
(*
  typed_function(M, A, B, r) ≡ is_function(M, r) ∧ is_relation(M, r) ∧
                                is_domain(M, r, A) ∧
            (∀u[M]. u ∈ r ⟶ (∀x[M]. ∀y[M]. pair(M, x, y, u) ⟶ y ∈ B))
*)

thm surjection_def
text‹@{thm [display] surjection_def}›
(*
  surjection(M, A, B, f) ≡ typed_function(M, A, B, f) ∧ (∀y[M]. y ∈ B ⟶
                              (∃x[M]. x ∈ A ∧ fun_apply(M, f, x, y)))
*)

text‹Internalized formulas›

thm Member Equal Nand Forall formula.induct
text‹@{thm [display] Member Equal Nand Forall formula.induct}›
(*
  x ∈ ω ⟹ y ∈ ω ⟹ Member(x, y) ∈ formula
  x ∈ ω ⟹ y ∈ ω ⟹ Equal(x, y) ∈ formula
  p ∈ formula ⟹ Forall(p) ∈ formula
  p ∈ formula ⟹ q ∈ formula ⟹ Nand(p, q) ∈ formula

  x ∈ formula ⟹
  (⋀x y. x ∈ ω ⟹ y ∈ ω ⟹ P(Member(x, y))) ⟹
  (⋀x y. x ∈ ω ⟹ y ∈ ω ⟹ P(Equal(x, y))) ⟹
  (⋀p q. p ∈ formula ⟹ P(p) ⟹ q ∈ formula ⟹ P(q) ⟹ P(Nand(p, q))) ⟹
  (⋀p. p ∈ formula ⟹ P(p) ⟹ P(Forall(p))) ⟹ P(x)
*)

thm arity.simps
text‹@{thm [display] arity.simps}›
(*
  arity(Member(x, y)) = succ(x) ∪ succ(y)
  arity(Equal(x, y)) = succ(x) ∪ succ(y)
  arity(Nand(p, q)) = arity(p) ∪ arity(q)
  arity(Forall(p)) = pred(arity(p))
*)

thm mem_iff_sats equal_iff_sats sats_Nand_iff sats_Forall_iff
text‹@{thm [display] mem_iff_sats equal_iff_sats sats_Nand_iff sats_Forall_iff}›
(*
  nth(i, env) = x ⟹ nth(j, env) = y ⟹ env ∈ list(A) ⟹ x ∈ y ⟷ A, env ⊨ Member(i, j)
  nth(i, env) = x ⟹ nth(j, env) = y ⟹ env ∈ list(A) ⟹ x = y ⟷ A, env ⊨ Equal(i, j)
  env ∈ list(A) ⟹ A, env ⊨ Nand(p, q) ⟷ ¬ (A, env ⊨ p ∧ A, env ⊨ q)
  env ∈ list(A) ⟹ A, env ⊨ Forall(p) ⟷ (∀x∈A. A, Cons(x, env) ⊨ p
*)

subsection‹Forcing \label{sec:def-main-forcing}›

thm infinity_ax_def
text‹@{thm [display] infinity_ax_def}›
(*
  infinity_ax(M) ≡ ∃I[M]. (∃z[M]. empty(M, z) ∧ z ∈ I) ∧ (∀y[M]. y ∈ I ⟶
                        (∃sy[M]. successor(M, y, sy) ∧ sy ∈ I))
*)

thm choice_ax_def
text‹@{thm [display] choice_ax_def}›
(*
  choice_ax(M) ≡ ∀x[M]. ∃a[M]. ∃f[M]. ordinal(M, a) ∧ surjection(M, a, x, f)
*)

thm ZF_union_fm_iff_sats ZF_power_fm_iff_sats ZF_pairing_fm_iff_sats
  ZF_foundation_fm_iff_sats ZF_extensionality_fm_iff_sats
  ZF_infinity_fm_iff_sats sats_ZF_separation_fm_iff
  sats_ZF_replacement_fm_iff ZF_choice_fm_iff_sats
text‹@{thm [display] ZF_union_fm_iff_sats ZF_power_fm_iff_sats
  ZF_pairing_fm_iff_sats
  ZF_foundation_fm_iff_sats ZF_extensionality_fm_iff_sats
  ZF_infinity_fm_iff_sats sats_ZF_separation_fm_iff
  sats_ZF_replacement_fm_iff ZF_choice_fm_iff_sats}›
(*
  Union_ax(##A) ⟷ A, [] ⊨ ZF_union_fm

  power_ax(##A) ⟷ A, [] ⊨ ZF_power_fm

  upair_ax(##A) ⟷ A, [] ⊨ ZF_pairing_fm

  foundation_ax(##A) ⟷ A, [] ⊨ ZF_foundation_fm

  extensionality(##A) ⟷ A, [] ⊨ ZF_extensionality_fm

  infinity_ax(##A) ⟷ A, [] ⊨ ZF_infinity_fm

  φ ∈ formula ⟹
    M, [] ⊨ ZF_separation_fm(φ) ⟷
    (∀env∈list(M). arity(φ) ≤ 1 #+ length(env) ⟶ separation(##M, λx. M, [x] @ env ⊨ φ))

  φ ∈ formula ⟹
    M, [] ⊨ ZF_replacement_fm(φ) ⟷
    (∀env∈list(M). arity(φ) ≤ 2 #+ length(env) ⟶ strong_replacement(##M, λx y. M, [x, y] @ env ⊨ φ))

  choice_ax(##A) ⟷ A, [] ⊨ ZF_choice_fm
*)

thm ZF_fin_def ZF_inf_def ZF_def ZFC_fin_def ZFC_def
text‹@{thm [display] ZF_fin_def ZF_inf_def ZF_def ZFC_fin_def
  ZFC_def}›
(*
  ZF_fin ≡ {ZF_extensionality_fm, ZF_foundation_fm, ZF_pairing_fm,
             ZF_union_fm, ZF_infinity_fm, ZF_power_fm}
  ZF_inf ≡ {ZF_separation_fm(p) . p ∈ formula} ∪ {ZF_replacement_fm(p) . p ∈ formula}
  ZF ≡ ZF_inf ∪ ZF_fin
  ZFC_fin ≡ ZF_fin ∪ {ZF_choice_fm}
  ZFC ≡ ZF_inf ∪ ZFC_fin
*)

thm satT_def
text‹@{thm [display] satT_def}›
(*
  A ⊨ Φ  ≡  ∀φ∈Φ. A, [] ⊨ φ
*)

thm extensions_of_ctms
text‹@{thm [display] extensions_of_ctms}›
(*
  M ≈ ω ⟹
  Transset(M) ⟹
  M ⊨ ZF ⟹
  ∃N. M ⊆ N ∧
      N ≈ ω ∧
      Transset(N) ∧ N ⊨ ZF ∧ M ≠ N ∧ (∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N)
        ∧ (M, [] ⊨ ZF_choice_fm ⟶ N ⊨ ZFC)
*)

end