Theory Fixed_Points
section ‹Fixed Points and Cantor's Theorems›
theory Fixed_Points
imports Axiom_Of_Choice Pred_Logic Cardinality
begin
text ‹The definitions below correspond to Definition 2.6.12 in Halvorson.›
definition fixed_point :: "cfunc ⇒ cfunc ⇒ bool" where
"fixed_point a g ⟷ (∃ A. g : A → A ∧ a ∈⇩c A ∧ g ∘⇩c a = a)"
definition has_fixed_point :: "cfunc ⇒ bool" where
"has_fixed_point g ⟷ (∃ a. fixed_point a g)"
definition fixed_point_property :: "cset ⇒ bool" where
"fixed_point_property A ⟷ (∀ g. g : A → A ⟶ has_fixed_point g)"
lemma fixed_point_def2:
assumes "g : A → A" "a ∈⇩c A"
shows "fixed_point a g = (g ∘⇩c a = a)"
unfolding fixed_point_def using assms by blast
text ‹The lemma below corresponds to Theorem 2.6.13 in Halvorson.›
lemma Lawveres_fixed_point_theorem:
assumes p_type[type_rule]: "p : X → A⇗X⇖"
assumes p_surj: "surjective p"
shows "fixed_point_property A"
unfolding fixed_point_property_def has_fixed_point_def
proof(clarify)
fix g
assume g_type[type_rule]: "g : A → A"
obtain φ where φ_def: "φ = p⇧♭"
by auto
then have φ_type[type_rule]: "φ : X ×⇩c X → A"
by (simp add: flat_type p_type)
obtain f where f_def: "f = g ∘⇩c φ ∘⇩c diagonal(X)"
by auto
then have f_type[type_rule]:"f : X → A"
using φ_type comp_type diagonal_type f_def g_type by blast
obtain x_f where x_f: "metafunc f = p ∘⇩c x_f" and x_f_type[type_rule]: "x_f ∈⇩c X"
using assms by (typecheck_cfuncs, metis p_surj surjective_def2)
have "φ⇘[-,x_f]⇙ = f"
proof(etcs_rule one_separator)
fix x
assume x_type[type_rule]: "x ∈⇩c X"
have "φ⇘[-,x_f]⇙ ∘⇩c x = φ ∘⇩c ⟨x, x_f⟩"
by (typecheck_cfuncs, meson right_param_on_el x_f)
also have "... = ((eval_func A X) ∘⇩c (id X ×⇩f p)) ∘⇩c ⟨x, x_f⟩"
using assms φ_def inv_transpose_func_def3 by auto
also have "... = (eval_func A X) ∘⇩c (id X ×⇩f p) ∘⇩c ⟨x, x_f⟩"
by (typecheck_cfuncs, metis comp_associative2)
also have "... = (eval_func A X) ∘⇩c ⟨id X ∘⇩c x, p ∘⇩c x_f⟩"
using cfunc_cross_prod_comp_cfunc_prod x_f by (typecheck_cfuncs, force)
also have "... = (eval_func A X) ∘⇩c ⟨x, metafunc f⟩"
using id_left_unit2 x_f by (typecheck_cfuncs, auto)
also have "... = f ∘⇩c x"
by (simp add: eval_lemma f_type x_type)
finally show "φ⇘[-,x_f]⇙ ∘⇩c x = f ∘⇩c x".
qed
then have "φ⇘[-,x_f]⇙ ∘⇩c x_f = g ∘⇩c φ ∘⇩c diagonal(X) ∘⇩c x_f"
by (typecheck_cfuncs, smt (z3) cfunc_type_def comp_associative domain_comp f_def x_f)
then have "φ ∘⇩c ⟨x_f, x_f⟩ = g ∘⇩c φ ∘⇩c ⟨x_f, x_f⟩"
using diag_on_elements right_param_on_el x_f by (typecheck_cfuncs, auto)
then have "fixed_point (φ ∘⇩c ⟨x_f, x_f⟩) g"
using fixed_point_def2 by (typecheck_cfuncs, auto)
then show "∃a. fixed_point a g"
using fixed_point_def by auto
qed
text ‹The theorem below corresponds to Theorem 2.6.14 in Halvorson.›
theorem Cantors_Negative_Theorem:
"∄ s. s : X → 𝒫 X ∧ surjective s"
proof(rule ccontr, clarify)
fix s
assume s_type: "s : X → 𝒫 X"
assume s_surj: "surjective s"
then have Omega_has_ffp: "fixed_point_property Ω"
using Lawveres_fixed_point_theorem powerset_def s_type by auto
have Omega_doesnt_have_ffp: "¬(fixed_point_property Ω)"
unfolding fixed_point_property_def has_fixed_point_def fixed_point_def
proof
assume BWOC: "∀g. g : Ω → Ω ⟶ (∃a A. g : A → A ∧ a ∈⇩c A ∧ g ∘⇩c a = a)"
have "NOT : Ω → Ω ∧ (∀a. ∀A. a ∈⇩c A ⟶ NOT : A → A ⟶ NOT ∘⇩c a ≠ a ∨ ¬ a ∈⇩c Ω)"
by (typecheck_cfuncs, metis AND_complementary AND_idempotent OR_complementary OR_idempotent true_false_distinct)
then have "∃g. g : Ω → Ω ∧ (∀a. ∀A. a ∈⇩c A ⟶ g : A → A ⟶ g ∘⇩c a ≠ a)"
by (metis cfunc_type_def)
then show False
using BWOC by presburger
qed
show False
using Omega_doesnt_have_ffp Omega_has_ffp by auto
qed
text ‹The theorem below corresponds to Exercise 2.6.15 in Halvorson.›
theorem Cantors_Positive_Theorem:
"∃m. m : X → Ω⇗X⇖ ∧ injective m"
proof -
have eq_pred_sharp_type[type_rule]: "eq_pred X⇧♯ : X → Ω⇗X⇖"
by typecheck_cfuncs
have "injective(eq_pred X⇧♯)"
unfolding injective_def
proof (clarify)
fix x y
assume "x ∈⇩c domain (eq_pred X⇧♯)" then have x_type[type_rule]: "x ∈⇩c X"
using cfunc_type_def eq_pred_sharp_type by auto
assume "y ∈⇩c domain (eq_pred X⇧♯)" then have y_type[type_rule]:"y ∈⇩c X"
using cfunc_type_def eq_pred_sharp_type by auto
assume eq: "eq_pred X⇧♯ ∘⇩c x = eq_pred X⇧♯ ∘⇩c y"
have "eq_pred X ∘⇩c ⟨x, x⟩ = eq_pred X ∘⇩c ⟨x, y⟩"
proof -
have "eq_pred X ∘⇩c ⟨x, x⟩ = ((eval_func Ω X) ∘⇩c (id X ×⇩f (eq_pred X⇧♯)) ) ∘⇩c ⟨x, x⟩"
using transpose_func_def by (typecheck_cfuncs, presburger)
also have "... = (eval_func Ω X) ∘⇩c (id X ×⇩f (eq_pred X⇧♯)) ∘⇩c ⟨x, x⟩"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (eval_func Ω X) ∘⇩c ⟨id X ∘⇩c x, (eq_pred X⇧♯) ∘⇩c x⟩"
using cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs, force)
also have "... = (eval_func Ω X) ∘⇩c ⟨id X ∘⇩c x, (eq_pred X⇧♯) ∘⇩c y⟩"
by (simp add: eq)
also have "... = (eval_func Ω X) ∘⇩c (id X ×⇩f (eq_pred X⇧♯)) ∘⇩c ⟨x, y⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = ((eval_func Ω X) ∘⇩c (id X ×⇩f (eq_pred X⇧♯)) ) ∘⇩c ⟨x, y⟩"
using comp_associative2 by (typecheck_cfuncs, blast)
also have "... = eq_pred X ∘⇩c ⟨x, y⟩"
using transpose_func_def by (typecheck_cfuncs, presburger)
finally show ?thesis.
qed
then show "x = y"
by (metis eq_pred_iff_eq x_type y_type)
qed
then show "∃m. m : X → Ω⇗X⇖ ∧ injective m"
using eq_pred_sharp_type injective_imp_monomorphism by blast
qed
text ‹The corollary below corresponds to Corollary 2.6.16 in Halvorson.›
corollary
"X ≤⇩c 𝒫 X ∧ ¬ (X ≅ 𝒫 X)"
using Cantors_Negative_Theorem Cantors_Positive_Theorem
unfolding is_smaller_than_def is_isomorphic_def powerset_def
by (metis epi_is_surj injective_imp_monomorphism iso_imp_epi_and_monic)
corollary Generalized_Cantors_Positive_Theorem:
assumes "¬ terminal_object Y"
assumes "¬ initial_object Y"
shows "X ≤⇩c Y⇗X⇖"
proof -
have "Ω ≤⇩c Y"
by (simp add: assms non_init_non_ter_sets)
then have fact: "Ω⇗X⇖ ≤⇩c Y⇗X⇖"
by (simp add: exp_preserves_card2)
have "X ≤⇩c Ω⇗X⇖"
by (meson Cantors_Positive_Theorem CollectI injective_imp_monomorphism is_smaller_than_def)
then show ?thesis
using fact set_card_transitive by blast
qed
corollary Generalized_Cantors_Negative_Theorem:
assumes "¬ initial_object X"
assumes "¬ terminal_object Y"
shows "∄ s. s : X → Y⇗X⇖ ∧ surjective s"
proof(rule ccontr, clarify)
fix s
assume s_type: "s : X → Y⇗X⇖"
assume s_surj: "surjective s"
obtain m where m_type: "m : Y⇗X⇖ → X" and m_mono: "monomorphism(m)"
by (meson epis_give_monos s_surj s_type surjective_is_epimorphism)
have "nonempty X"
using is_empty_def assms(1) iso_empty_initial no_el_iff_iso_empty nonempty_def by blast
then have nonempty: "nonempty (Ω⇗X⇖)"
using nonempty_def nonempty_to_nonempty true_func_type by blast
show False
proof(cases "initial_object Y")
assume "initial_object Y"
then have "Y⇗X⇖ ≅ ∅"
by (simp add: ‹nonempty X› empty_to_nonempty initial_iso_empty no_el_iff_iso_empty)
then show False
by (meson is_empty_def assms(1) comp_type iso_empty_initial no_el_iff_iso_empty s_type)
next
assume "¬ initial_object Y"
then have "Ω ≤⇩c Y"
by (simp add: assms(2) non_init_non_ter_sets)
then obtain n where n_type: "n : Ω⇗X⇖ → Y⇗X⇖" and n_mono: "monomorphism(n)"
by (meson exp_preserves_card2 is_smaller_than_def)
then have mn_type: "m ∘⇩c n : Ω⇗X⇖ → X"
by (meson comp_type m_type)
have mn_mono: "monomorphism(m ∘⇩c n)"
using cfunc_type_def composition_of_monic_pair_is_monic m_mono m_type n_mono n_type by presburger
then have "∃g. g: X → Ω⇗X⇖ ∧ epimorphism(g) ∧ g ∘⇩c (m ∘⇩c n) = id (Ω⇗X⇖)"
by (simp add: mn_type monos_give_epis nonempty)
then show False
by (metis Cantors_Negative_Theorem epi_is_surj powerset_def)
qed
qed
end