section ‹Soundness› theory Soundness imports Elementary_Logic Semantics begin no_notation funcset (infixr "→" 60) notation funcset (infixr "⇸" 60) subsection ‹Proposition 5400› proposition (in general_model) prop_5400: assumes "A ∈ wffs⇘α⇙" and "φ ↝ 𝒟" and "ψ ↝ 𝒟" and "∀v ∈ free_vars A. φ v = ψ v" shows "𝒱 φ A = 𝒱 ψ A" proof - from assms(1) show ?thesis using assms(2,3,4) proof (induction A arbitrary: φ ψ) case (var_is_wff α x) have "(x, α) ∈ free_vars (x⇘α⇙)" by simp from assms(1) and var_is_wff.prems(1) have "𝒱 φ (x⇘α⇙) = φ (x, α)" using 𝒱_is_wff_denotation_function by fastforce also from ‹(x, α) ∈ free_vars (x⇘α⇙)› and var_is_wff.prems(3) have "… = ψ (x, α)" by (simp only:) also from assms(1) and var_is_wff.prems(2) have "… = 𝒱 ψ (x⇘α⇙)" using 𝒱_is_wff_denotation_function by fastforce finally show ?case . next case (con_is_wff α c) from assms(1) and con_is_wff.prems(1) have "𝒱 φ (⦃c⦄⇘α⇙) = 𝒥 (c, α)" using 𝒱_is_wff_denotation_function by fastforce also from assms(1) and con_is_wff.prems(2) have "… = 𝒱 ψ (⦃c⦄⇘α⇙)" using 𝒱_is_wff_denotation_function by fastforce finally show ?case . next case (app_is_wff α β A B) have "free_vars (A · B) = free_vars A ∪ free_vars B" by simp with app_is_wff.prems(3) have "∀v ∈ free_vars A. φ v = ψ v" and "∀v ∈ free_vars B. φ v = ψ v" by blast+ with app_is_wff.IH and app_is_wff.prems(1,2) have "𝒱 φ A = 𝒱 ψ A" and "𝒱 φ B = 𝒱 ψ B" by blast+ from assms(1) and app_is_wff.prems(1) and app_is_wff.hyps have "𝒱 φ (A · B) = 𝒱 φ A ∙ 𝒱 φ B" using 𝒱_is_wff_denotation_function by fastforce also from ‹𝒱 φ A = 𝒱 ψ A› and ‹𝒱 φ B = 𝒱 ψ B› have "… = 𝒱 ψ A ∙ 𝒱 ψ B" by (simp only:) also from assms(1) and app_is_wff.prems(2) and app_is_wff.hyps have "… = 𝒱 ψ (A · B)" using 𝒱_is_wff_denotation_function by fastforce finally show ?case . next case (abs_is_wff β A α x) have "free_vars (λx⇘α⇙. A) = free_vars A - {(x, α)}" by simp with abs_is_wff.prems(3) have "∀v ∈ free_vars A. v ≠ (x, α)⟶ φ v = ψ v" by blast then have "∀v ∈ free_vars A. (φ((x, α) := z)) v = (ψ((x, α) := z)) v" if "z ∈ elts (𝒟 α)" for z by simp moreover from abs_is_wff.prems(1,2) have "∀x' α'. (φ((x, α) := z)) (x', α') ∈ elts (𝒟 α')" (* needs α-conversion *) and "∀x' α'. (ψ((x, α) := z)) (x', α') ∈ elts (𝒟 α')" (* needs α-conversion *) if "z ∈ elts (𝒟 α)" for z using that by force+ ultimately have 𝒱_φ_ψ_eq: "𝒱 (φ((x, α) := z)) A = 𝒱 (ψ((x, α) := z)) A" if "z ∈ elts (𝒟 α)" for z using abs_is_wff.IH and that by simp from assms(1) and abs_is_wff.prems(1) and abs_is_wff.hyps have "𝒱 φ (λx⇘α⇙. A) = (❙λz ❙:𝒟 α❙.𝒱 (φ((x, α) := z)) A)" using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by simp also from 𝒱_φ_ψ_eq have "… = (❙λz ❙:𝒟 α❙.𝒱 (ψ((x, α) := z)) A)" by (fact vlambda_extensionality) also from assms(1) and abs_is_wff.hyps have "… = 𝒱 ψ (λx⇘α⇙. A)" using wff_abs_denotation[OF 𝒱_is_wff_denotation_function abs_is_wff.prems(2)] by simp finally show ?case . qed qed corollary (in general_model) closed_wff_is_meaningful_regardless_of_assignment: assumes "is_closed_wff_of_type A α" and "φ ↝ 𝒟" and "ψ ↝ 𝒟" shows "𝒱 φ A = 𝒱 ψ A" using assms and prop_5400 by blast subsection ‹Proposition 5401› lemma (in general_model) prop_5401_a: assumes "φ ↝ 𝒟" and "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘β⇙" shows "𝒱 φ ((λx⇘α⇙. B) · A) = 𝒱 (φ((x, α) := 𝒱 φ A)) B" proof - from assms(2,3) have "λx⇘α⇙. B ∈ wffs⇘α→β⇙" by blast with assms(1,2) have "𝒱 φ ((λx⇘α⇙. B) · A) = 𝒱 φ (λx⇘α⇙. B) ∙ 𝒱 φ A" using 𝒱_is_wff_denotation_function by blast also from assms(1,3) have "… = app (❙λz ❙:𝒟 α❙.𝒱 (φ((x, α) := z)) B) (𝒱 φ A)" using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by simp also from assms(1,2) have "… = 𝒱 (φ((x, α) := 𝒱 φ A)) B" using 𝒱_is_wff_denotation_function by auto finally show ?thesis . qed lemma (in general_model) prop_5401_b: assumes "φ ↝ 𝒟" and "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙" shows "𝒱 φ (A =⇘α⇙ B) = ❙T⟷ 𝒱 φ A = 𝒱 φ B" proof - from assms have "{𝒱 φ A, 𝒱 φ B} ⊆ elts (𝒟 α)" using 𝒱_is_wff_denotation_function by auto have "𝒱 φ (A =⇘α⇙ B) = 𝒱 φ (Q⇘α⇙ · A · B)" by simp also from assms have "… = 𝒱 φ (Q⇘α⇙ · A) ∙ 𝒱 φ B" using 𝒱_is_wff_denotation_function by blast also from assms have "… = 𝒱 φ (Q⇘α⇙) ∙ 𝒱 φ A ∙ 𝒱 φ B" using Q_wff and wff_app_denotation[OF 𝒱_is_wff_denotation_function] by fastforce also from assms(1) have "… = (q⇘α⇙) ∙ 𝒱 φ A ∙ 𝒱 φ B" using Q_denotation and 𝒱_is_wff_denotation_function by fastforce also from ‹{𝒱 φ A, 𝒱 φ B} ⊆ elts (𝒟 α)› have "… = ❙T⟷ 𝒱 φ A = 𝒱 φ B" using q_is_equality by simp finally show ?thesis . qed corollary (in general_model) prop_5401_b': assumes "φ ↝ 𝒟" and "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙" shows "𝒱 φ (A ≡⇧^{𝒬}B) = ❙T⟷ 𝒱 φ A = 𝒱 φ B" using assms and prop_5401_b by auto lemma (in general_model) prop_5401_c: assumes "φ ↝ 𝒟" shows "𝒱 φ T⇘_{o}⇙ = ❙T" proof - have "Q⇘o⇙ ∈ wffs⇘o→o→o⇙" by blast moreover have "𝒱 φ T⇘_{o}⇙ = 𝒱 φ (Q⇘o⇙ =⇘o→o→o⇙ Q⇘o⇙)" unfolding true_def .. ultimately have "… = ❙T⟷ 𝒱 φ (Q⇘o⇙) = 𝒱 φ (Q⇘o⇙)" using prop_5401_b and assms by blast then show ?thesis by simp qed lemma (in general_model) prop_5401_d: assumes "φ ↝ 𝒟" shows "𝒱 φ F⇘_{o}⇙ = ❙F" proof - have "λ𝔵⇘o⇙. T⇘o⇙ ∈ wffs⇘o→o⇙" and "λ𝔵⇘o⇙. 𝔵⇘o⇙ ∈ wffs⇘o→o⇙" by blast+ moreover have "𝒱 φ F⇘_{o}⇙ = 𝒱 φ (λ𝔵⇘o⇙. T⇘o⇙ =⇘o→o⇙ λ𝔵⇘o⇙. 𝔵⇘o⇙)" unfolding false_def .. ultimately have "𝒱 φ F⇘_{o}⇙ = ❙T⟷ 𝒱 φ (λ𝔵⇘o⇙. T⇘o⇙) = 𝒱 φ (λ𝔵⇘o⇙. 𝔵⇘o⇙)" using prop_5401_b and assms by simp moreover have "𝒱 φ (λ𝔵⇘o⇙. T⇘o⇙) ≠ 𝒱 φ (λ𝔵⇘o⇙. 𝔵⇘o⇙)" proof - have "𝒱 φ (λ𝔵⇘o⇙. T⇘o⇙) = (❙λz ❙:𝒟 o❙.❙T)" proof - from assms have T_denotation: "𝒱 (φ((𝔵, o) := z)) T⇘_{o}⇙ = ❙T" if "z ∈ elts (𝒟 o)" for z using prop_5401_c and that by simp from assms have "𝒱 φ (λ𝔵⇘o⇙. T⇘o⇙) = (❙λz ❙:𝒟 o❙.𝒱 (φ((𝔵, o) := z)) T⇘_{o}⇙)" using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by blast also from assms and T_denotation have "… = (❙λz ❙:𝒟 o❙.❙T)" using vlambda_extensionality by fastforce finally show ?thesis . qed moreover have "𝒱 φ (λ𝔵⇘o⇙. 𝔵⇘o⇙) = (❙λz ❙:𝒟 o❙.z)" proof - from assms have 𝔵_denotation: "𝒱 (φ((𝔵, o) := z)) (𝔵⇘o⇙) = z" if "z ∈ elts (𝒟 o)" for z using that and 𝒱_is_wff_denotation_function by auto from assms have "𝒱 φ (λ𝔵⇘o⇙. 𝔵⇘o⇙) = (❙λz ❙:𝒟 o❙.𝒱 (φ((𝔵, o) := z)) (𝔵⇘o⇙))" using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by blast also from 𝔵_denotation have "… = (❙λz ❙:(𝒟 o)❙.z)" using vlambda_extensionality by fastforce finally show ?thesis . qed moreover have "(❙λz ❙:𝒟 o❙.❙T) ≠ (❙λz ❙:𝒟 o❙.z)" proof - from assms(1) have "(❙λz ❙:𝒟 o❙.❙T) ∙ ❙F= ❙T" by (simp add: truth_values_domain_def) moreover from assms(1) have "(❙λz ❙:𝒟 o❙.z) ∙ ❙F= ❙F" by (simp add: truth_values_domain_def) ultimately show ?thesis by (auto simp add: inj_eq) qed ultimately show ?thesis by simp qed moreover from assms have "𝒱 φ F⇘_{o}⇙ ∈ elts (𝒟 o)" using false_wff and 𝒱_is_wff_denotation_function by fast ultimately show ?thesis using assms(1) by (simp add: truth_values_domain_def) qed lemma (in general_model) prop_5401_e: assumes "φ ↝ 𝒟" and "{x, y} ⊆ elts (𝒟 o)" shows "𝒱 φ (∧⇘_{o→o→o}⇙) ∙ x ∙ y = (if x = ❙T∧ y = ❙Tthen ❙Telse ❙F)" proof - let ?B⇩_{l}⇩_{e}⇩_{q}= "λ𝔤⇘o→o→o⇙. 𝔤⇘o→o→o⇙ · T⇘_{o}⇙ · T⇘_{o}⇙" let ?B⇩_{r}⇩_{e}⇩_{q}= "λ𝔤⇘o→o→o⇙. 𝔤⇘o→o→o⇙ · 𝔵⇘o⇙ · 𝔶⇘o⇙" let ?B⇩_{e}⇩_{q}= "?B⇩_{l}⇩_{e}⇩_{q}=⇘(o→o→o)→o⇙ ?B⇩_{r}⇩_{e}⇩_{q}" let ?B⇩_{𝔶}= "λ𝔶⇘o⇙. ?B⇩_{e}⇩_{q}" let ?B⇩_{𝔵}= "λ𝔵⇘o⇙. ?B⇩_{𝔶}" let ?φ' = "φ((𝔵, o) := x, (𝔶, o) := y)" let ?φ'' = "λg. ?φ'((𝔤, o→o→o) := g)" have "𝔤⇘o→o→o⇙ · T⇘_{o}⇙ ∈ wffs⇘o→o⇙" by blast have "𝔤⇘o→o→o⇙ · T⇘_{o}⇙ · T⇘_{o}⇙ ∈ wffs⇘o⇙" and "𝔤⇘o→o→o⇙ · 𝔵⇘o⇙ · 𝔶⇘o⇙ ∈ wffs⇘o⇙" by blast+ have "?B⇩_{l}⇩_{e}⇩_{q}∈ wffs⇘(o→o→o)→o⇙" and "?B⇩_{r}⇩_{e}⇩_{q}∈ wffs⇘(o→o→o)→o⇙" by blast+ then have "?B⇩_{e}⇩_{q}∈ wffs⇘o⇙" and "?B⇩_{𝔶}∈ wffs⇘o→o⇙" and "?B⇩_{𝔵}∈ wffs⇘o→o→o⇙" by blast+ have "𝒱 φ (∧⇘_{o→o→o}⇙) ∙ x ∙ y = 𝒱 φ ?B⇩_{𝔵}∙ x ∙ y" by simp also from assms and ‹?B⇩_{𝔶}∈ wffs⇘o→o⇙› have "… = 𝒱 (φ((𝔵, o) := x)) ?B⇩_{𝔶}∙ y" using mixed_beta_conversion by simp also from assms and ‹?B⇩_{e}⇩_{q}∈ wffs⇘o⇙› have "… = 𝒱 ?φ' ?B⇩_{e}⇩_{q}" using mixed_beta_conversion by simp finally have "𝒱 φ (∧⇘_{o→o→o}⇙) ∙ x ∙ y = ❙T⟷ 𝒱 ?φ' ?B⇩_{l}⇩_{e}⇩_{q}= 𝒱 ?φ' ?B⇩_{r}⇩_{e}⇩_{q}" using assms and ‹?B⇩_{l}⇩_{e}⇩_{q}∈ wffs⇘(o→o→o)→o⇙› and ‹?B⇩_{r}⇩_{e}⇩_{q}∈ wffs⇘(o→o→o)→o⇙› and prop_5401_b by simp also have "… ⟷ (❙λg ❙:𝒟 (o→o→o)❙.g ∙ ❙T∙ ❙T) = (❙λg ❙:𝒟 (o→o→o)❙.g ∙ x ∙ y)" proof - have leq: "𝒱 ?φ' ?B⇩_{l}⇩_{e}⇩_{q}= (❙λg ❙:𝒟 (o→o→o)❙.g ∙ ❙T∙ ❙T)" and req: "𝒱 ?φ' ?B⇩_{r}⇩_{e}⇩_{q}= (❙λg ❙:𝒟 (o→o→o)❙.g ∙ x ∙ y)" proof - from assms(1,2) have is_assg_φ'': "?φ'' g ↝ 𝒟" if "g ∈ elts (𝒟 (o→o→o))" for g using that by auto have side_eq_denotation: "𝒱 ?φ' (λ𝔤⇘o→o→o⇙. 𝔤⇘o→o→o⇙ · A · B) = (❙λg ❙:𝒟 (o→o→o)❙.g ∙ 𝒱 (?φ'' g) A ∙ 𝒱 (?φ'' g) B)" if "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙" for A and B proof - from that have "𝔤⇘o→o→o⇙ · A · B ∈ wffs⇘o⇙" by blast have "𝒱 (?φ'' g) (𝔤⇘o→o→o⇙ · A · B) = g ∙ 𝒱 (?φ'' g) A ∙ 𝒱 (?φ'' g) B" if "g ∈ elts (𝒟 (o→o→o))" for g proof - from ‹A ∈ wffs⇘o⇙› have "𝔤⇘o→o→o⇙ · A ∈ wffs⇘o→o⇙" by blast with that and is_assg_φ'' and ‹B ∈ wffs⇘o⇙› have " 𝒱 (?φ'' g) (𝔤⇘o→o→o⇙ · A · B) = 𝒱 (?φ'' g) (𝔤⇘o→o→o⇙ · A) ∙ 𝒱 (?φ'' g) B" using wff_app_denotation[OF 𝒱_is_wff_denotation_function] by simp also from that and ‹A ∈ wffs⇘o⇙› and is_assg_φ'' have " … = 𝒱 (?φ'' g) (𝔤⇘o→o→o⇙) ∙ 𝒱 (?φ'' g) A ∙ 𝒱 (?φ'' g) B" by (metis 𝒱_is_wff_denotation_function wff_app_denotation wffs_of_type_intros(1)) finally show ?thesis using that and is_assg_φ'' and 𝒱_is_wff_denotation_function by auto qed moreover from assms have "is_assignment ?φ'" by auto with ‹𝔤⇘o→o→o⇙ · A · B ∈ wffs⇘o⇙› have " 𝒱 ?φ' (λ𝔤⇘o→o→o⇙. 𝔤⇘o→o→o⇙ · A · B) = (❙λg ❙:𝒟 (o→o→o)❙.𝒱 (?φ'' g) (𝔤⇘o→o→o⇙ · A · B))" using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by simp ultimately show ?thesis using vlambda_extensionality by fastforce qed ― ‹Proof of ‹leq›:› show "𝒱 ?φ' ?B⇩_{l}⇩_{e}⇩_{q}= (❙λg ❙:𝒟 (o→o→o)❙.g ∙ ❙T∙ ❙T)" proof - have "𝒱 (?φ'' g) T⇘_{o}⇙ = ❙T" if "g ∈ elts (𝒟 (o→o→o))" for g using that and is_assg_φ'' and prop_5401_c by simp then show ?thesis using side_eq_denotation and true_wff and vlambda_extensionality by fastforce qed ― ‹Proof of ‹req›:› show "𝒱 ?φ' ?B⇩_{r}⇩_{e}⇩_{q}= (❙λg ❙:𝒟 (o→o→o)❙.g ∙ x ∙ y)" proof - from is_assg_φ'' have "𝒱 (?φ'' g) (𝔵⇘o⇙) = x" and "𝒱 (?φ'' g) (𝔶⇘o⇙) = y" if "g ∈ elts (𝒟 (o→o→o))" for g using that and 𝒱_is_wff_denotation_function by auto with side_eq_denotation show ?thesis using wffs_of_type_intros(1) and vlambda_extensionality by fastforce qed qed then show ?thesis by auto qed also have "… ⟷ (∀g ∈ elts (𝒟 (o→o→o)). g ∙ ❙T∙ ❙T= g ∙ x ∙ y)" using vlambda_extensionality and VLambda_eq_D2 by fastforce finally have and_eqv: " 𝒱 φ (∧⇘_{o→o→o}⇙) ∙ x ∙ y = ❙T⟷ (∀g ∈ elts (𝒟 (o→o→o)). g ∙ ❙T∙ ❙T= g ∙ x ∙ y)" by blast then show ?thesis proof - from assms(1,2) have is_assg_1: "φ((𝔵, o) := ❙T) ↝ 𝒟" by (simp add: truth_values_domain_def) then have is_assg_2: "φ((𝔵, o) := ❙T, (𝔶, o) := ❙T) ↝ 𝒟" unfolding is_assignment_def by (metis fun_upd_apply prod.sel(2)) from assms consider (a) "x = ❙T∧ y = ❙T" | (b) "x ≠ ❙T" | (c) "y ≠ ❙T" by blast then show ?thesis proof cases case a then have "g ∙ ❙T∙ ❙T= g ∙ x ∙ y" if "g ∈ elts (𝒟 (o→o→o))" for g by simp with a and and_eqv show ?thesis by simp next case b let ?g_witness = "λ𝔵⇘o⇙. λ𝔶⇘o⇙. 𝔵⇘o⇙" have "λ𝔶⇘o⇙. 𝔵⇘o⇙ ∈ wffs⇘o→o⇙" by blast then have "is_closed_wff_of_type ?g_witness (o→o→o)" by force moreover from assms have is_assg_φ': "?φ' ↝ 𝒟" by simp ultimately have "𝒱 φ ?g_witness ∙ ❙T∙ ❙T= 𝒱 ?φ' ?g_witness ∙ ❙T∙ ❙T" using assms(1) and closed_wff_is_meaningful_regardless_of_assignment by metis also from assms and ‹λ𝔶⇘o⇙. 𝔵⇘o⇙ ∈ wffs⇘o→o⇙› have " 𝒱 ?φ' ?g_witness ∙ ❙T∙ ❙T= 𝒱 (?φ'((𝔵, o) := ❙T)) (λ𝔶⇘o⇙. 𝔵⇘o⇙) ∙ ❙T" using mixed_beta_conversion and truth_values_domain_def by auto also from assms(1) and ‹λ𝔶⇘o⇙. 𝔵⇘o⇙ ∈ wffs⇘o→o⇙› and is_assg_1 and calculation have " … = 𝒱 (?φ'((𝔵, o) := ❙T, (𝔶, o) := ❙T)) (𝔵⇘o⇙)" using mixed_beta_conversion and is_assignment_def by (metis fun_upd_same fun_upd_twist fun_upd_upd wffs_of_type_intros(1)) also have "… = ❙T" using is_assg_2 and 𝒱_is_wff_denotation_function by fastforce finally have "𝒱 φ ?g_witness ∙ ❙T∙ ❙T= ❙T" . with b have "𝒱 φ ?g_witness ∙ ❙T∙ ❙T≠ x" by blast moreover have "x = 𝒱 φ ?g_witness ∙ x ∙ y" proof - from is_assg_φ' have "x = 𝒱 ?φ' (𝔵⇘o⇙)" using 𝒱_is_wff_denotation_function by auto also from assms(2) and is_assg_φ' have "… = 𝒱 ?φ' (λ𝔶⇘o⇙. 𝔵⇘o⇙) ∙ y" using wffs_of_type_intros(1)[where x = 𝔵 and α = o] by (simp add: mixed_beta_conversion 𝒱_is_wff_denotation_function) also from assms(2) have "… = 𝒱 ?φ' ?g_witness ∙ x ∙ y" using is_assg_φ' and ‹λ𝔶⇘o⇙. 𝔵⇘o⇙ ∈ wffs⇘o→o⇙› by (simp add: mixed_beta_conversion fun_upd_twist) also from assms(1,2) have "… = 𝒱 φ ?g_witness ∙ x ∙ y" using is_assg_φ' and ‹is_closed_wff_of_type ?g_witness (o→o→o)› and closed_wff_is_meaningful_regardless_of_assignment by metis finally show ?thesis . qed moreover from assms(1,2) have "𝒱 φ ?g_witness ∈ elts (𝒟 (o→o→o))" using ‹is_closed_wff_of_type ?g_witness (o→o→o)› and 𝒱_is_wff_denotation_function by simp ultimately have "∃g ∈ elts (𝒟 (o→o→o)). g ∙ ❙T∙ ❙T≠ g ∙ x ∙ y" by auto moreover from assms have "𝒱 φ (∧⇘_{o→o→o}⇙) ∙ x ∙ y ∈ elts (𝒟 o)" by (rule fully_applied_conj_fun_is_domain_respecting) ultimately have "𝒱 φ (∧⇘_{o→o→o}⇙) ∙ x ∙ y = ❙F" using and_eqv and truth_values_domain_def by fastforce with b show ?thesis by simp next case c let ?g_witness = "λ𝔵⇘o⇙. λ𝔶⇘o⇙. 𝔶⇘o⇙" have "λ𝔶⇘o⇙. 𝔶⇘o⇙ ∈ wffs⇘o→o⇙" by blast then have "is_closed_wff_of_type ?g_witness (o→o→o)" by force moreover from assms(1,2) have is_assg_φ': "?φ' ↝ 𝒟" by simp ultimately have "𝒱 φ ?g_witness ∙ ❙T∙ ❙T= 𝒱 ?φ' ?g_witness ∙ ❙T∙ ❙T" using assms(1) and closed_wff_is_meaningful_regardless_of_assignment by metis also from is_assg_1 and is_assg_φ' have "… = 𝒱 (?φ'((𝔵, o) := ❙T)) (λ𝔶⇘o⇙. 𝔶⇘o⇙) ∙ ❙T" using ‹λ𝔶⇘o⇙. 𝔶⇘o⇙ ∈ wffs⇘o→o⇙› and mixed_beta_conversion and truth_values_domain_def by auto also from assms(1) and ‹λ𝔶⇘o⇙. 𝔶⇘o⇙ ∈ wffs⇘o→o⇙› and is_assg_1 and calculation have " … = 𝒱 (?φ'((𝔵, o) := ❙T, (𝔶, o) := ❙T)) (𝔶⇘o⇙)" using mixed_beta_conversion and is_assignment_def by (metis fun_upd_same fun_upd_twist fun_upd_upd wffs_of_type_intros(1)) also have "… = ❙T" using is_assg_2 and 𝒱_is_wff_denotation_function by force finally have "𝒱 φ ?g_witness ∙ ❙T∙ ❙T= ❙T" . with c have "𝒱 φ ?g_witness ∙ ❙T∙ ❙T≠ y" by blast moreover have "y = 𝒱 φ ?g_witness ∙ x ∙ y" proof - from assms(2) and is_assg_φ' have "y = 𝒱 ?φ' (λ𝔶⇘o⇙. 𝔶⇘o⇙) ∙ y" using wffs_of_type_intros(1)[where x = 𝔶 and α = o] and 𝒱_is_wff_denotation_function and mixed_beta_conversion by auto also from assms(2) and ‹λ𝔶⇘o⇙. 𝔶⇘o⇙ ∈ wffs⇘o→o⇙› have "… = 𝒱 ?φ' ?g_witness ∙ x ∙ y" using is_assg_φ' by (simp add: mixed_beta_conversion fun_upd_twist) also from assms(1,2) have "… = 𝒱 φ ?g_witness ∙ x ∙ y" using is_assg_φ' and ‹is_closed_wff_of_type ?g_witness (o→o→o)› and closed_wff_is_meaningful_regardless_of_assignment by metis finally show ?thesis . qed moreover from assms(1) have "𝒱 φ ?g_witness ∈ elts (𝒟 (o→o→o))" using ‹is_closed_wff_of_type ?g_witness (o→o→o)› and 𝒱_is_wff_denotation_function by auto ultimately have "∃g ∈ elts (𝒟 (o→o→o)). g ∙ ❙T∙ ❙T≠ g ∙ x ∙ y" by auto moreover from assms have "𝒱 φ (∧⇘_{o→o→o}⇙) ∙ x ∙ y ∈ elts (𝒟 o)" by (rule fully_applied_conj_fun_is_domain_respecting) ultimately have "𝒱 φ (∧⇘_{o→o→o}⇙) ∙ x ∙ y = ❙F" using and_eqv and truth_values_domain_def by fastforce with c show ?thesis by simp qed qed qed corollary (in general_model) prop_5401_e': assumes "φ ↝ 𝒟" and "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙" shows "𝒱 φ (A ∧⇧^{𝒬}B) = 𝒱 φ A ❙∧𝒱 φ B" proof - from assms have "{𝒱 φ A, 𝒱 φ B} ⊆ elts (𝒟 o)" using 𝒱_is_wff_denotation_function by simp from assms(2) have "∧⇘_{o→o→o}⇙ · A ∈ wffs⇘o→o⇙" by blast have "𝒱 φ (A ∧⇧^{𝒬}B) = 𝒱 φ (∧⇘_{o→o→o}⇙ · A · B)" by simp also from assms have "… = 𝒱 φ (∧⇘_{o→o→o}⇙ · A) ∙ 𝒱 φ B" using 𝒱_is_wff_denotation_function and ‹∧⇘_{o→o→o}⇙ · A ∈ wffs⇘o→o⇙› by blast also from assms have "… = 𝒱 φ (∧⇘_{o→o→o}⇙) ∙ 𝒱 φ A ∙ 𝒱 φ B" using 𝒱_is_wff_denotation_function and conj_fun_wff by fastforce also from assms(1,2) have "… = (if 𝒱 φ A = ❙T∧ 𝒱 φ B = ❙Tthen ❙Telse ❙F)" using ‹{𝒱 φ A, 𝒱 φ B} ⊆ elts (𝒟 o)› and prop_5401_e by simp also have "… = 𝒱 φ A ❙∧𝒱 φ B" using truth_values_domain_def and ‹{𝒱 φ A, 𝒱 φ B} ⊆ elts (𝒟 o)› by fastforce finally show ?thesis . qed lemma (in general_model) prop_5401_f: assumes "φ ↝ 𝒟" and "{x, y} ⊆ elts (𝒟 o)" shows "𝒱 φ (⊃⇘_{o→o→o}⇙) ∙ x ∙ y = (if x = ❙T∧ y = ❙Fthen ❙Felse ❙T)" proof - let ?φ' = "φ((𝔵, o) := x, (𝔶, o) := y)" from assms(2) have "{x, y} ⊆ elts 𝔹" unfolding truth_values_domain_def . have "(𝔵⇘o⇙ ≡⇧^{𝒬}𝔵⇘o⇙ ∧⇧^{𝒬}𝔶⇘o⇙) ∈ wffs⇘o⇙" by blast then have "λ𝔶⇘o⇙. (𝔵⇘o⇙ ≡⇧^{𝒬}𝔵⇘o⇙ ∧⇧^{𝒬}𝔶⇘o⇙) ∈ wffs⇘o→o⇙" by blast from assms have is_assg_φ': "?φ' ↝ 𝒟" by simp from assms(1) have "𝒱 ?φ' (𝔵⇘o⇙) = x" and "𝒱 ?φ' (𝔶⇘o⇙) = y" using is_assg_φ' and 𝒱_is_wff_denotation_function by force+ have "𝒱 φ (⊃⇘_{o→o→o}⇙) ∙ x ∙ y = 𝒱 φ (λ𝔵⇘o⇙. λ𝔶⇘o⇙. (𝔵⇘o⇙ ≡⇧^{𝒬}𝔵⇘o⇙ ∧⇧^{𝒬}𝔶⇘o⇙)) ∙ x ∙ y" by simp also from assms have "… = 𝒱 (φ((𝔵, o) := x)) (λ𝔶⇘o⇙. (𝔵⇘o⇙ ≡⇧^{𝒬}𝔵⇘o⇙ ∧⇧^{𝒬}𝔶⇘o⇙)) ∙ y" using ‹λ𝔶⇘o⇙. (𝔵⇘o⇙ ≡⇧^{𝒬}𝔵⇘o⇙ ∧⇧^{𝒬}𝔶⇘o⇙) ∈ wffs⇘o→o⇙› and mixed_beta_conversion by simp also from assms have "… = 𝒱 ?φ' (𝔵⇘o⇙ ≡⇧^{𝒬}𝔵⇘o⇙ ∧⇧^{𝒬}𝔶⇘o⇙)" using mixed_beta_conversion and ‹(𝔵⇘o⇙ ≡⇧^{𝒬}𝔵⇘o⇙ ∧⇧^{𝒬}𝔶⇘o⇙) ∈ wffs⇘o⇙› by simp finally have "𝒱 φ (⊃⇘_{o→o→o}⇙) ∙ x ∙ y = ❙T⟷ 𝒱 ?φ' (𝔵⇘o⇙) = 𝒱 ?φ' (𝔵⇘o⇙ ∧⇧^{𝒬}𝔶⇘o⇙)" using prop_5401_b'[OF is_assg_φ'] and conj_op_wff and wffs_of_type_intros(1) by simp also have "… ⟷ x = x ❙∧y" unfolding prop_5401_e'[OF is_assg_φ' wffs_of_type_intros(1) wffs_of_type_intros(1)] and ‹𝒱 ?φ' (𝔵⇘o⇙) = x› and ‹𝒱 ?φ' (𝔶⇘o⇙) = y› .. also have "… ⟷ x = (if x = ❙T∧ y = ❙Tthen ❙Telse ❙F)" using ‹{x, y} ⊆ elts 𝔹› by auto also have "… ⟷ ❙T= (if x = ❙T∧ y = ❙Fthen ❙Felse ❙T)" using ‹{x, y} ⊆ elts 𝔹› by auto finally show ?thesis using assms and fully_applied_imp_fun_denotation_is_domain_respecting and tv_cases and truth_values_domain_def by metis qed corollary (in general_model) prop_5401_f': assumes "φ ↝ 𝒟" and "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙" shows "𝒱 φ (A ⊃⇧^{𝒬}B) = 𝒱 φ A ❙⊃𝒱 φ B" proof - from assms have "{𝒱 φ A, 𝒱 φ B} ⊆ elts (𝒟 o)" using 𝒱_is_wff_denotation_function by simp from assms(2) have "⊃⇘_{o→o→o}⇙ · A ∈ wffs⇘o→o⇙" by blast have "𝒱 φ (A ⊃⇧^{𝒬}B) = 𝒱 φ (⊃⇘_{o→o→o}⇙ · A · B)" by simp also from assms(1,3) have "… = 𝒱 φ (⊃⇘_{o→o→o}⇙ · A) ∙ 𝒱 φ B" using 𝒱_is_wff_denotation_function and ‹⊃⇘_{o→o→o}⇙ · A ∈ wffs⇘o→o⇙› by blast also from assms have "… = 𝒱 φ (⊃⇘_{o→o→o}⇙) ∙ 𝒱 φ A ∙ 𝒱 φ B" using 𝒱_is_wff_denotation_function and imp_fun_wff by fastforce also from assms have "… = (if 𝒱 φ A = ❙T∧ 𝒱 φ B = ❙Fthen ❙Felse ❙T)" using ‹{𝒱 φ A, 𝒱 φ B} ⊆ elts (𝒟 o)› and prop_5401_f by simp also have "… = 𝒱 φ A ❙⊃𝒱 φ B" using truth_values_domain_def and ‹{𝒱 φ A, 𝒱 φ B} ⊆ elts (𝒟 o)› by auto finally show ?thesis . qed lemma (in general_model) forall_denotation: assumes "φ ↝ 𝒟" and "A ∈ wffs⇘o⇙" shows "𝒱 φ (∀x⇘α⇙. A) = ❙T⟷ (∀z ∈ elts (𝒟 α). 𝒱 (φ((x, α) := z)) A = ❙T)" proof - from assms(1) have lhs: "𝒱 φ (λ𝔵⇘α⇙. T⇘o⇙) ∙ z = ❙T" if "z ∈ elts (𝒟 α)" for z using prop_5401_c and mixed_beta_conversion and that and true_wff by simp from assms have rhs: "𝒱 φ (λx⇘α⇙. A) ∙ z = 𝒱 (φ((x, α) := z)) A" if "z ∈ elts (𝒟 α)" for z using that by (simp add: mixed_beta_conversion) from assms(2) have "λ𝔵⇘α⇙. T⇘o⇙ ∈ wffs⇘α→o⇙" and "λx⇘α⇙. A ∈ wffs⇘α→o⇙" by auto have "𝒱 φ (∀x⇘α⇙. A) = 𝒱 φ (∏⇘α⇙ · (λx⇘α⇙. A))" unfolding forall_def .. also have "… = 𝒱 φ (Q⇘α→o⇙ · (λ𝔵⇘α⇙. T⇘o⇙) · (λx⇘α⇙. A))" unfolding PI_def .. also have "… = 𝒱 φ ((λ𝔵⇘α⇙. T⇘o⇙) =⇘α→o⇙ (λx⇘α⇙. A))" unfolding equality_of_type_def .. finally have "𝒱 φ (∀x⇘α⇙. A) = 𝒱 φ ((λ𝔵⇘α⇙. T⇘o⇙) =⇘α→o⇙ (λx⇘α⇙. A))" . moreover from assms(1,2) have " 𝒱 φ ((λ𝔵⇘α⇙. T⇘o⇙) =⇘α→o⇙ (λx⇘α⇙. A)) = ❙T⟷ 𝒱 φ (λ𝔵⇘α⇙. T⇘o⇙) = 𝒱 φ (λx⇘α⇙. A)" using ‹λ𝔵⇘α⇙. T⇘o⇙ ∈ wffs⇘α→o⇙› and ‹λx⇘α⇙. A ∈ wffs⇘α→o⇙› and prop_5401_b by blast moreover have "(𝒱 φ (λ𝔵⇘α⇙. T⇘o⇙) = 𝒱 φ (λx⇘α⇙. A)) ⟷ (∀z ∈ elts (𝒟 α). 𝒱 (φ((x, α) := z)) A = ❙T)" proof assume "𝒱 φ (λ𝔵⇘α⇙. T⇘o⇙) = 𝒱 φ (λx⇘α⇙. A)" with lhs and rhs show "∀z ∈ elts (𝒟 α). 𝒱 (φ((x, α) := z)) A = ❙T" by auto next assume "∀z ∈ elts (𝒟 α). 𝒱 (φ((x, α) := z)) A = ❙T" moreover from assms have "𝒱 φ (λ𝔵⇘α⇙. T⇘o⇙) = (❙λz ❙:𝒟 α❙.𝒱 (φ((𝔵, α) := z)) T⇘_{o}⇙)" using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by blast moreover from assms have "𝒱 φ (λx⇘α⇙. A) = (❙λz ❙:𝒟 α❙.𝒱 (φ((x, α) := z)) A)" using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by blast ultimately show "𝒱 φ (λ𝔵⇘α⇙. T⇘o⇙) = 𝒱 φ (λx⇘α⇙. A)" using lhs and vlambda_extensionality by fastforce qed ultimately show ?thesis by (simp only:) qed lemma prop_5401_g: assumes "is_general_model ℳ" and "φ ↝⇩_{M}ℳ" and "A ∈ wffs⇘o⇙" shows "ℳ ⊨⇘φ⇙ ∀x⇘α⇙. A ⟷ (∀ψ. ψ ↝⇩_{M}ℳ ∧ ψ ∼⇘(x, α)⇙ φ ⟶ ℳ ⊨⇘ψ⇙ A)" proof - obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)" using prod_cases3 by blast with assms have " ℳ ⊨⇘φ⇙ ∀x⇘α⇙. A ⟷ ∀x⇘α⇙. A ∈ wffs⇘o⇙ ∧ is_general_model (𝒟, 𝒥, 𝒱) ∧ φ ↝ 𝒟 ∧ 𝒱 φ (∀x⇘α⇙. A) = ❙T" by fastforce also from assms and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "… ⟷ (∀z ∈ elts (𝒟 α). 𝒱 (φ((x, α) := z)) A = ❙T)" using general_model.forall_denotation by fastforce also have "… ⟷ (∀ψ. ψ ↝ 𝒟 ∧ ψ ∼⇘(x, α)⇙ φ ⟶ ℳ ⊨⇘ψ⇙ A)" proof assume *: "∀z ∈ elts (𝒟 α). 𝒱 (φ((x, α) := z)) A = ❙T" { fix ψ assume "ψ ↝ 𝒟" and "ψ ∼⇘(x, α)⇙ φ" have "𝒱 ψ A = ❙T" proof - have "∃z ∈ elts (𝒟 α). ψ = φ((x, α) := z)" proof (rule ccontr) assume "¬ (∃z ∈ elts (𝒟 α). ψ = φ((x, α) := z))" with ‹ψ ∼⇘(x, α)⇙ φ› have "∀z ∈ elts (𝒟 α). ψ (x, α) ≠ z" by fastforce then have "ψ (x, α) ∉ elts (𝒟 α)" by blast moreover from assms(1) and ‹ℳ = (𝒟, 𝒥, 𝒱)› and ‹ψ ↝ 𝒟› have "ψ (x, α) ∈ elts (𝒟 α)" using general_model_def and premodel_def and frame.is_assignment_def by auto ultimately show False by simp qed with * show ?thesis by fastforce qed with assms(1) and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "ℳ ⊨⇘ψ⇙ A" by simp } then show "∀ψ. ψ ↝ 𝒟 ∧ ψ ∼⇘(x, α)⇙ φ ⟶ ℳ ⊨⇘ψ⇙ A" by blast next assume *: "∀ψ. ψ ↝ 𝒟 ∧ ψ ∼⇘(x, α)⇙ φ ⟶ ℳ ⊨⇘ψ⇙ A" show "∀z ∈ elts (𝒟 α). 𝒱 (φ((x, α) := z)) A = ❙T" proof fix z assume "z ∈ elts (𝒟 α)" with assms(1,2) and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "φ((x, α) := z) ↝ 𝒟" using general_model_def and premodel_def and frame.is_assignment_def by auto moreover have "φ((x, α) := z) ∼⇘(x, α)⇙ φ" by simp ultimately have "ℳ ⊨⇘φ((x, α) := z)⇙ A" using * by blast with assms(1) and ‹ℳ = (𝒟, 𝒥, 𝒱)› and ‹φ((x, α) := z) ↝ 𝒟› show "𝒱 (φ((x, α) := z)) A = ❙T" by simp qed qed finally show ?thesis using ‹ℳ = (𝒟, 𝒥, 𝒱)› by simp qed lemma (in general_model) axiom_1_validity_aux: assumes "φ ↝ 𝒟" shows "𝒱 φ (𝔤⇘o→o⇙ · T⇘_{o}⇙ ∧⇧^{𝒬}𝔤⇘o→o⇙ · F⇘_{o}⇙ ≡⇧^{𝒬}∀𝔵⇘o⇙. 𝔤⇘o→o⇙ · 𝔵⇘o⇙) = ❙T" (is "𝒱 φ (?A ≡⇧^{𝒬}?B) = ❙T") proof - let ?ℳ = "(𝒟, 𝒥, 𝒱)" from assms have *: "is_general_model ?ℳ" "φ ↝⇩_{M}?ℳ" using general_model_axioms by blast+ have "?A ≡⇧^{𝒬}?B ∈ wffs⇘o⇙" using axioms.axiom_1 and axioms_are_wffs_of_type_o by blast have lhs: "𝒱 φ ?A = φ (𝔤, o→o) ∙ ❙T❙∧φ (𝔤, o→o) ∙ ❙F" proof - have "𝔤⇘o→o⇙ · T⇘_{o}⇙ ∈ wffs⇘o⇙" and "𝔤⇘o→o⇙ · F⇘_{o}⇙ ∈ wffs⇘o⇙" by blast+ with assms have "𝒱 φ ?A = 𝒱 φ (𝔤⇘o→o⇙ · T⇘_{o}⇙) ❙∧𝒱 φ (𝔤⇘o→o⇙ · F⇘_{o}⇙)" using prop_5401_e' by simp also from assms have "… = φ (𝔤, o→o) ∙ 𝒱 φ (T⇘_{o}⇙) ❙∧φ (𝔤, o→o) ∙ 𝒱 φ (F⇘_{o}⇙)" using wff_app_denotation[OF 𝒱_is_wff_denotation_function] and wff_var_denotation[OF 𝒱_is_wff_denotation_function] by (metis false_wff true_wff wffs_of_type_intros(1)) finally show ?thesis using assms and prop_5401_c and prop_5401_d by simp qed have "𝒱 φ (?A ≡⇧^{𝒬}?B) = ❙T" proof (cases "∀z ∈ elts (𝒟 o). φ (𝔤, o→o) ∙ z = ❙T") case True with assms have "φ (𝔤, o→o) ∙ ❙T= ❙T" and "φ (𝔤, o→o) ∙ ❙F= ❙T" using truth_values_domain_def by auto with lhs have "𝒱 φ ?A = ❙T❙∧❙T" by (simp only:) also have "… = ❙T" by simp finally have "𝒱 φ ?A = ❙T" . moreover have "𝒱 φ ?B = ❙T" proof - have "𝔤⇘o→o⇙ · 𝔵⇘o⇙ ∈ wffs⇘o⇙" by blast moreover { fix ψ assume "ψ ↝ 𝒟" and "ψ ∼⇘(𝔵, o)⇙ φ" with assms have "𝒱 ψ (𝔤⇘o→o⇙ · 𝔵⇘o⇙) = 𝒱 ψ (𝔤⇘o→o⇙) ∙ 𝒱 ψ (𝔵⇘o⇙)" using 𝒱_is_wff_denotation_function by blast also from ‹ψ ↝ 𝒟› have "… = ψ (𝔤, o→o) ∙ ψ (𝔵, o)" using 𝒱_is_wff_denotation_function by auto also from ‹ψ ∼⇘(𝔵, o)⇙ φ› have "… = φ (𝔤, o→o) ∙ ψ (𝔵, o)" by simp also from True and ‹ψ ↝ 𝒟› have "… = ❙T" by blast finally have "𝒱 ψ (𝔤⇘o→o⇙ · 𝔵⇘o⇙) = ❙T" . with assms and ‹𝔤⇘o→o⇙ · 𝔵⇘o⇙ ∈ wffs⇘o⇙› have "?ℳ ⊨⇘ψ⇙ 𝔤⇘o→o⇙ · 𝔵⇘o⇙" by simp } ultimately have "?ℳ ⊨⇘φ⇙ ?B" using assms and * and prop_5401_g by auto with *(2) show ?thesis by simp qed ultimately show ?thesis using assms and prop_5401_b' and wffs_from_equivalence[OF ‹?A ≡⇧^{𝒬}?B ∈ wffs⇘o⇙›] by simp next case False then have "∃z ∈ elts (𝒟 o). φ (𝔤, o→o) ∙ z ≠ ❙T" by blast moreover from * have "∀z ∈ elts (𝒟 o). φ (𝔤, o→o) ∙ z ∈ elts (𝒟 o)" using app_is_domain_respecting by blast ultimately obtain z where "z ∈ elts (𝒟 o)" and "φ (𝔤, o→o) ∙ z = ❙F" using truth_values_domain_def by auto define ψ where ψ_def: "ψ = φ((𝔵, o) := z)" with * and ‹z ∈ elts (𝒟 o)› have "ψ ↝ 𝒟" by simp then have "𝒱 ψ (𝔤⇘o→o⇙ · 𝔵⇘o⇙) = 𝒱 ψ (𝔤⇘o→o⇙) ∙ 𝒱 ψ (𝔵⇘o⇙)" using 𝒱_is_wff_denotation_function by blast also from ‹ψ ↝ 𝒟› have "… = ψ (𝔤, o→o) ∙ ψ (𝔵, o)" using 𝒱_is_wff_denotation_function by auto also from ψ_def have "… = φ (𝔤, o→o) ∙ z" by simp also have "… = ❙F" unfolding ‹φ (𝔤, o→o) ∙ z = ❙F› .. finally have "𝒱 ψ (𝔤⇘o→o⇙ · 𝔵⇘o⇙) = ❙F" . with ‹ψ ↝ 𝒟› have "¬ ?ℳ ⊨⇘ψ⇙ 𝔤⇘o→o⇙ · 𝔵⇘o⇙" by (auto simp add: inj_eq) with ‹ψ ↝ 𝒟› and ψ_def have "¬ (∀ψ. ψ ↝ 𝒟 ∧ ψ ∼⇘(𝔵, o)⇙ φ ⟶ ?ℳ ⊨⇘ψ⇙ 𝔤⇘o→o⇙ · 𝔵⇘o⇙)" using fun_upd_other by fastforce with ‹¬ ?ℳ ⊨⇘ψ⇙ 𝔤⇘o→o⇙ · 𝔵⇘o⇙› have "¬ ?ℳ ⊨⇘φ⇙ ?B" using prop_5401_g[OF * wffs_from_forall[OF wffs_from_equivalence(2)[OF ‹?A ≡⇧^{𝒬}?B ∈ wffs⇘o⇙›]]] by blast then have "𝒱 φ (∀𝔵⇘o⇙. 𝔤⇘o→o⇙ · 𝔵⇘o⇙) ≠ ❙T" by simp moreover from assms have "𝒱 φ ?B ∈ elts (𝒟 o)" using wffs_from_equivalence[OF ‹?A ≡⇧^{𝒬}?B ∈ wffs⇘o⇙›] and 𝒱_is_wff_denotation_function by auto ultimately have "𝒱 φ ?B = ❙F" by (simp add: truth_values_domain_def) moreover have "𝒱 φ (𝔤⇘o→o⇙ · T⇘_{o}⇙ ∧⇧^{𝒬}𝔤⇘o→o⇙ · F⇘_{o}⇙) = ❙F" proof - from ‹z ∈ elts (𝒟 o)› and ‹φ (𝔤, o→o) ∙ z = ❙F› have "((φ (𝔤, o→o)) ∙ ❙T) = ❙F∨ ((φ (𝔤, o→o)) ∙ ❙F) = ❙F" using truth_values_domain_def by fastforce moreover from ‹z ∈ elts (𝒟 o)› and ‹φ (𝔤, o→o) ∙ z = ❙F› and ‹∀z ∈ elts (𝒟 o). φ (𝔤, o→o) ∙ z ∈ elts (𝒟 o)› have "{(φ (𝔤, o→o)) ∙ ❙T, (φ (𝔤, o→o)) ∙ ❙F} ⊆ elts (𝒟 o)" by (simp add: truth_values_domain_def) ultimately have "((φ (𝔤, o→o)) ∙ ❙T) ❙∧((φ (𝔤, o→o)) ∙ ❙F) = ❙F" by auto with lhs show ?thesis by (simp only:) qed ultimately show ?thesis using assms and prop_5401_b' and wffs_from_equivalence[OF ‹?A ≡⇧^{𝒬}?B ∈ wffs⇘o⇙›] by simp qed then show ?thesis . qed lemma axiom_1_validity: shows "⊨ 𝔤⇘o→o⇙ · T⇘_{o}⇙ ∧⇧^{𝒬}𝔤⇘o→o⇙ · F⇘_{o}⇙ ≡⇧^{𝒬}∀𝔵⇘o⇙. 𝔤⇘o→o⇙ · 𝔵⇘o⇙" (is "⊨ ?A ≡⇧^{𝒬}?B") proof (intro allI impI) fix ℳ and φ assume *: "is_general_model ℳ" "φ ↝⇩_{M}ℳ" show "ℳ ⊨⇘φ⇙ ?A ≡⇧^{𝒬}?B" proof - obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)" using prod_cases3 by blast moreover from * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ (?A ≡⇧^{𝒬}?B) = ❙T" using general_model.axiom_1_validity_aux by simp ultimately show ?thesis by simp qed qed lemma (in general_model) axiom_2_validity_aux: assumes "φ ↝ 𝒟" shows "𝒱 φ ((𝔵⇘α⇙ =⇘α⇙ 𝔶⇘α⇙) ⊃⇧^{𝒬}(𝔥⇘α→o⇙ · 𝔵⇘α⇙ ≡⇧^{𝒬}𝔥⇘α→o⇙ · 𝔶⇘α⇙)) = ❙T" (is "𝒱 φ (?A ⊃⇧^{𝒬}?B) = ❙T") proof - have "?A ⊃⇧^{𝒬}?B ∈ wffs⇘o⇙" using axioms.axiom_2 and axioms_are_wffs_of_type_o by blast from ‹?A ⊃⇧^{𝒬}?B ∈ wffs⇘o⇙› have "?A ∈ wffs⇘o⇙" and "?B ∈ wffs⇘o⇙" using wffs_from_imp_op by blast+ with assms have "𝒱 φ (?A ⊃⇧^{𝒬}?B) = 𝒱 φ ?A ❙⊃𝒱 φ ?B" using prop_5401_f' by simp moreover from assms and ‹?A ∈ wffs⇘o⇙› and ‹?B ∈ wffs⇘o⇙› have "{𝒱 φ ?A, 𝒱 φ ?B} ⊆ elts (𝒟 o)" using 𝒱_is_wff_denotation_function by simp then have "{𝒱 φ ?A, 𝒱 φ ?B} ⊆ elts 𝔹" by (simp add: truth_values_domain_def) ultimately have 𝒱_imp_T: "𝒱 φ (?A ⊃⇧^{𝒬}?B) = ❙T⟷ 𝒱 φ ?A = ❙F∨ 𝒱 φ ?B = ❙T" by fastforce then show ?thesis proof (cases "φ (𝔵, α) = φ (𝔶, α)") case True from assms and ‹?B ∈ wffs⇘o⇙› have "𝒱 φ ?B = ❙T⟷ 𝒱 φ (𝔥⇘α→o⇙ · 𝔵⇘α⇙) = 𝒱 φ (𝔥⇘α→o⇙ · 𝔶⇘α⇙)" using wffs_from_equivalence and prop_5401_b' by metis moreover have "𝒱 φ (𝔥⇘α→o⇙ · 𝔵⇘α⇙) = 𝒱 φ (𝔥⇘α→o⇙ · 𝔶⇘α⇙)" proof - from assms and ‹?B ∈ wffs⇘o⇙› have "𝒱 φ (𝔥⇘α→o⇙ · 𝔵⇘α⇙) = 𝒱 φ (𝔥⇘α→o⇙) ∙ 𝒱 φ (𝔵⇘α⇙)" using 𝒱_is_wff_denotation_function by blast also from assms have "… = φ (𝔥, α→o) ∙ φ (𝔵, α)" using 𝒱_is_wff_denotation_function by auto also from True have "… = φ (𝔥, α→o) ∙ φ (𝔶, α)" by (simp only:) also from assms have "… = 𝒱 φ (𝔥⇘α→o⇙) ∙ 𝒱 φ (𝔶⇘α⇙)" using 𝒱_is_wff_denotation_function by auto also from assms and ‹?B ∈ wffs⇘o⇙› have "… = 𝒱 φ (𝔥⇘α→o⇙ · 𝔶⇘α⇙)" using wff_app_denotation[OF 𝒱_is_wff_denotation_function] by (metis wffs_of_type_intros(1)) finally show ?thesis . qed ultimately show ?thesis using 𝒱_imp_T by simp next case False from assms have "𝒱 φ ?A = ❙T⟷ 𝒱 φ (𝔵⇘α⇙) = 𝒱 φ (𝔶⇘α⇙)" using prop_5401_b by blast moreover from False and assms have "𝒱 φ (𝔵⇘α⇙) ≠ 𝒱 φ (𝔶⇘α⇙)" using 𝒱_is_wff_denotation_function by auto ultimately have "𝒱 φ ?A = ❙F" using assms and ‹{𝒱 φ ?A, 𝒱 φ ?B} ⊆ elts 𝔹› by simp then show ?thesis using 𝒱_imp_T by simp qed qed lemma axiom_2_validity: shows "⊨ (𝔵⇘α⇙ =⇘α⇙ 𝔶⇘α⇙) ⊃⇧^{𝒬}(𝔥⇘α→o⇙ · 𝔵⇘α⇙ ≡⇧^{𝒬}𝔥⇘α→o⇙ · 𝔶⇘α⇙)" (is "⊨ ?A ⊃⇧^{𝒬}?B") proof (intro allI impI) fix ℳ and φ assume *: "is_general_model ℳ" "φ ↝⇩_{M}ℳ" show "ℳ ⊨⇘φ⇙ ?A ⊃⇧^{𝒬}?B" proof - obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)" using prod_cases3 by blast moreover from * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ (?A ⊃⇧^{𝒬}?B) = ❙T" using general_model.axiom_2_validity_aux by simp ultimately show ?thesis by force qed qed lemma (in general_model) axiom_3_validity_aux: assumes "φ ↝ 𝒟" shows "𝒱 φ ((𝔣⇘α→β⇙ =⇘α→β⇙ 𝔤⇘α→β⇙) ≡⇧^{𝒬}∀𝔵⇘α⇙. (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙)) = ❙T" (is "𝒱 φ (?A ≡⇧^{𝒬}?B) = ❙T") proof - let ?ℳ = "(𝒟, 𝒥, 𝒱)" from assms have *: "is_general_model ?ℳ" "φ ↝⇩_{M}?ℳ" using general_model_axioms by blast+ have B'_wffo: "𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙ ∈ wffs⇘o⇙" by blast have "?A ≡⇧^{𝒬}?B ∈ wffs⇘o⇙" and "?A ∈ wffs⇘o⇙" and "?B ∈ wffs⇘o⇙" proof - show "?A ≡⇧^{𝒬}?B ∈ wffs⇘o⇙" using axioms.axiom_3 and axioms_are_wffs_of_type_o by blast then show "?A ∈ wffs⇘o⇙" and "?B ∈ wffs⇘o⇙" by (blast dest: wffs_from_equivalence)+ qed have "𝒱 φ ?A = 𝒱 φ ?B" proof (cases "φ (𝔣, α→β) = φ (𝔤, α→β)") case True have "𝒱 φ ?A = ❙T" proof - from assms have "𝒱 φ (𝔣⇘α→β⇙) = φ (𝔣, α→β)" using 𝒱_is_wff_denotation_function by auto also from True have "… = φ (𝔤, α→β)" by (simp only:) also from assms have "… = 𝒱 φ (𝔤⇘α→β⇙)" using 𝒱_is_wff_denotation_function by auto finally have "𝒱 φ (𝔣⇘α→β⇙) = 𝒱 φ (𝔤⇘α→β⇙)" . with assms show ?thesis using prop_5401_b by blast qed moreover have "𝒱 φ ?B = ❙T" proof - { fix ψ assume "ψ ↝ 𝒟" and "ψ ∼⇘(𝔵, α)⇙ φ" from assms and ‹ψ ↝ 𝒟› have "𝒱 ψ (𝔣⇘α→β⇙ · 𝔵⇘α⇙) = 𝒱 ψ (𝔣⇘α→β⇙) ∙ 𝒱 ψ (𝔵⇘α⇙)" using 𝒱_is_wff_denotation_function by blast also from assms and ‹ψ ↝ 𝒟› have "… = ψ (𝔣, α→β) ∙ ψ (𝔵, α)" using 𝒱_is_wff_denotation_function by auto also from ‹ψ ∼⇘(𝔵, α)⇙ φ› have "… = φ (𝔣, α→β) ∙ ψ (𝔵, α)" by simp also from True have "… = φ (𝔤, α→β) ∙ ψ (𝔵, α)" by (simp only:) also from ‹ψ ∼⇘(𝔵, α)⇙ φ› have "… = ψ (𝔤, α→β) ∙ ψ (𝔵, α)" by simp also from assms and ‹ψ ↝ 𝒟› have "… = 𝒱 ψ (𝔤⇘α→β⇙) ∙ 𝒱 ψ (𝔵⇘α⇙)" using 𝒱_is_wff_denotation_function by auto also from assms and ‹ψ ↝ 𝒟› have "… = 𝒱 ψ (𝔤⇘α→β⇙ · 𝔵⇘α⇙)" using wff_app_denotation[OF 𝒱_is_wff_denotation_function] by (metis wffs_of_type_intros(1)) finally have "𝒱 ψ (𝔣⇘α→β⇙ · 𝔵⇘α⇙) = 𝒱 ψ (𝔤⇘α→β⇙ · 𝔵⇘α⇙)" . with B'_wffo and assms and ‹ψ ↝ 𝒟› have "𝒱 ψ (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙) = ❙T" using prop_5401_b and wffs_from_equality by blast with *(2) have "?ℳ ⊨⇘ψ⇙ 𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙" by simp } with * and B'_wffo have "?ℳ ⊨⇘φ⇙ ?B" using prop_5401_g by force with *(2) show ?thesis by auto qed ultimately show ?thesis .. next case False from * have "φ (𝔣, α→β) ∈ elts (𝒟 α ⟼ 𝒟 β)" and "φ (𝔤, α→β) ∈ elts (𝒟 α ⟼ 𝒟 β)" by (simp_all add: function_domainD) with False obtain z where "z ∈ elts (𝒟 α)" and "φ (𝔣, α→β) ∙ z ≠ φ (𝔤, α→β) ∙ z" by (blast dest: fun_ext) define ψ where "ψ = φ((𝔵, α) := z)" from * and ‹z ∈ elts (𝒟 α)› have "ψ ↝ 𝒟" and "ψ ∼⇘(𝔵, α)⇙ φ" unfolding ψ_def by fastforce+ have "𝒱 ψ (f⇘α→β⇙ · 𝔵⇘α⇙) = φ (f, α→β) ∙ z" for f proof - from ‹ψ ↝ 𝒟› have "𝒱 ψ (f⇘α→β⇙ · 𝔵⇘α⇙) = 𝒱 ψ (f⇘α→β⇙) ∙ 𝒱 ψ (𝔵⇘α⇙)" using 𝒱_is_wff_denotation_function by blast also from ‹ψ ↝ 𝒟› have "… = ψ (f, α→β) ∙ ψ (𝔵, α)" using 𝒱_is_wff_denotation_function by auto finally show ?thesis unfolding ψ_def by simp qed then have "𝒱 ψ (𝔣⇘α→β⇙ · 𝔵⇘α⇙) = φ (𝔣, α→β) ∙ z" and "𝒱 ψ (𝔤⇘α→β⇙ · 𝔵⇘α⇙) = φ (𝔤, α→β) ∙ z" by (simp_all only:) with ‹φ (𝔣, α→β) ∙ z ≠ φ (𝔤, α→β) ∙ z› have "𝒱 ψ (𝔣⇘α→β⇙ · 𝔵⇘α⇙) ≠ 𝒱 ψ (𝔤⇘α→β⇙ · 𝔵⇘α⇙)" by simp then have "𝒱 ψ (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙) = ❙F" proof - from B'_wffo and ‹ψ ↝ 𝒟› and * have "𝒱 ψ (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙) ∈ elts (𝒟 o)" using 𝒱_is_wff_denotation_function by auto moreover from B'_wffo have "{𝔣⇘α→β⇙ · 𝔵⇘α⇙, 𝔤⇘α→β⇙ · 𝔵⇘α⇙} ⊆ wffs⇘β⇙" by blast with ‹ψ ↝ 𝒟› and ‹𝒱 ψ (𝔣⇘α→β⇙ · 𝔵⇘α⇙) ≠ 𝒱 ψ (𝔤⇘α→β⇙ · 𝔵⇘α⇙)› and B'_wffo have "𝒱 ψ (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙) ≠ ❙T" using prop_5401_b by simp ultimately show ?thesis by (simp add: truth_values_domain_def) qed with ‹ψ ↝ 𝒟› have "¬ ?ℳ ⊨⇘ψ⇙ 𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙" by (auto simp add: inj_eq) with ‹ψ ↝ 𝒟› and ‹ψ ∼⇘(𝔵, α)⇙ φ› have "∃ψ. ψ ↝ 𝒟 ∧ ψ ∼⇘(𝔵, α)⇙ φ ∧ ¬ ?ℳ ⊨⇘ψ⇙ 𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙" by blast with * and B'_wffo have "¬ ?ℳ ⊨⇘φ⇙ ?B" using prop_5401_g by blast then have "𝒱 φ ?B = ❙F" proof - from ‹?B ∈ wffs⇘o⇙› and * have "𝒱 φ ?B ∈ elts (𝒟 o)" using 𝒱_is_wff_denotation_function by auto with ‹¬ ?ℳ ⊨⇘φ⇙ ?B› and ‹?B ∈ wffs⇘o⇙› show ?thesis using truth_values_domain_def by fastforce qed moreover have "𝒱 φ (𝔣⇘α→β⇙ =⇘α→β⇙ 𝔤⇘α→β⇙) = ❙F" proof - from * have "𝒱 φ (𝔣⇘α→β⇙) = φ (𝔣, α→β)" and "𝒱 φ (𝔤⇘α→β⇙) = φ (𝔤, α→β)" using 𝒱_is_wff_denotation_function by auto with False have "𝒱 φ (𝔣⇘α→β⇙) ≠ 𝒱 φ (𝔤⇘α→β⇙)" by simp with * have "𝒱 φ (𝔣⇘α→β⇙ =⇘α→β⇙ 𝔤⇘α→β⇙) ≠ ❙T" using prop_5401_b by blast moreover from * and ‹?A ∈ wffs⇘o⇙› have "𝒱 φ (𝔣⇘α→β⇙ =⇘α→β⇙ 𝔤⇘α→β⇙) ∈ elts (𝒟 o)" using 𝒱_is_wff_denotation_function by auto ultimately show ?thesis by (simp add: truth_values_domain_def) qed ultimately show ?thesis by (simp only:) qed with * and ‹?A ∈ wffs⇘o⇙› and ‹?B ∈ wffs⇘o⇙› show ?thesis using prop_5401_b' by simp qed lemma axiom_3_validity: shows "⊨ (𝔣⇘α→β⇙ =⇘α→β⇙ 𝔤⇘α→β⇙) ≡⇧^{𝒬}∀𝔵⇘α⇙. (𝔣⇘α→β⇙ · 𝔵⇘α⇙ =⇘β⇙ 𝔤⇘α→β⇙ · 𝔵⇘α⇙)" (is "⊨ ?A ≡⇧^{𝒬}?B") proof (intro allI impI) fix ℳ and φ assume *: "is_general_model ℳ" "φ ↝⇩_{M}ℳ" show "ℳ ⊨⇘φ⇙ ?A ≡⇧^{𝒬}?B" proof - obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)" using prod_cases3 by blast moreover from * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ (?A ≡⇧^{𝒬}?B) = ❙T" using general_model.axiom_3_validity_aux by simp ultimately show ?thesis by simp qed qed lemma (in general_model) axiom_4_1_con_validity_aux: assumes "φ ↝ 𝒟" and "A ∈ wffs⇘α⇙" shows "𝒱 φ ((λx⇘α⇙. ⦃c⦄⇘β⇙) · A =⇘β⇙ ⦃c⦄⇘β⇙) = ❙T" proof - from assms(2) have "(λx⇘α⇙. ⦃c⦄⇘β⇙) · A =⇘β⇙ ⦃c⦄⇘β⇙ ∈ wffs⇘o⇙" using axioms.axiom_4_1_con and axioms_are_wffs_of_type_o by blast define ψ where "ψ = φ((x, α) := 𝒱 φ A)" from assms have "𝒱 φ ((λx⇘α⇙. ⦃c⦄⇘β⇙) · A) = 𝒱 (φ((x, α) := 𝒱 φ A)) (⦃c⦄⇘β⇙)" using prop_5401_a by blast also have "… = 𝒱 ψ (⦃c⦄⇘β⇙)" unfolding ψ_def .. also from assms and ψ_def have "… = 𝒱 φ (⦃c⦄⇘β⇙)" using 𝒱_is_wff_denotation_function by auto finally have "𝒱 φ ((λx⇘α⇙. ⦃c⦄⇘β⇙) · A) = 𝒱 φ (⦃c⦄⇘β⇙)" . with assms(1) and ‹(λx⇘α⇙. ⦃c⦄⇘β⇙) · A =⇘β⇙ ⦃c⦄⇘β⇙ ∈ wffs⇘o⇙› show ?thesis using wffs_from_equality(1) and prop_5401_b by blast qed lemma axiom_4_1_con_validity: assumes "A ∈ wffs⇘α⇙" shows "⊨ (λx⇘α⇙. ⦃c⦄⇘β⇙) · A =⇘β⇙ ⦃c⦄⇘β⇙" proof (intro allI impI) fix ℳ and φ assume *: "is_general_model ℳ" "φ ↝⇩_{M}ℳ" show "ℳ ⊨⇘φ⇙ (λx⇘α⇙. ⦃c⦄⇘β⇙) · A =⇘β⇙ ⦃c⦄⇘β⇙" proof - obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)" using prod_cases3 by blast moreover from assms and * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ ((λx⇘α⇙. ⦃c⦄⇘β⇙) · A =⇘β⇙ ⦃c⦄⇘β⇙) = ❙T" using general_model.axiom_4_1_con_validity_aux by simp ultimately show ?thesis by simp qed qed lemma (in general_model) axiom_4_1_var_validity_aux: assumes "φ ↝ 𝒟" and "A ∈ wffs⇘α⇙" and "(y, β) ≠ (x, α)" shows "𝒱 φ ((λx⇘α⇙. y⇘β⇙) · A =⇘β⇙ y⇘β⇙) = ❙T" proof - from assms(2) have "(λx⇘α⇙. y⇘β⇙) · A =⇘β⇙ y⇘β⇙ ∈ wffs⇘o⇙" using axioms.axiom_4_1_var and axioms_are_wffs_of_type_o by blast define ψ where "ψ = φ((x, α) := 𝒱 φ A)" with assms(1,2) have "𝒱 φ ((λx⇘α⇙. y⇘β⇙) · A) = 𝒱 (φ((x, α) := 𝒱 φ A)) (y⇘β⇙)" using prop_5401_a by blast also have "… = 𝒱 ψ (y⇘β⇙)" unfolding ψ_def .. also have "… = 𝒱 φ (y⇘β⇙)" proof - from assms(1,2) have "𝒱 φ A ∈ elts (𝒟 α)" using 𝒱_is_wff_denotation_function by auto with ψ_def and assms(1) have "ψ ↝ 𝒟" by simp moreover have "free_vars (y⇘β⇙) = {(y, β)}" by simp with ψ_def and assms(3) have "∀v ∈ free_vars (y⇘β⇙). φ v = ψ v" by auto ultimately show ?thesis using prop_5400[OF wffs_of_type_intros(1) assms(1)] by simp qed finally have "𝒱 φ ((λx⇘α⇙. y⇘β⇙) · A) = 𝒱 φ (y⇘β⇙)" . with ‹(λx⇘α⇙. y⇘β⇙) · A =⇘β⇙ y⇘β⇙ ∈ wffs⇘o⇙› show ?thesis using wffs_from_equality(1) and prop_5401_b[OF assms(1)] by blast qed lemma axiom_4_1_var_validity: assumes "A ∈ wffs⇘α⇙" and "(y, β) ≠ (x, α)" shows "⊨ (λx⇘α⇙. y⇘β⇙) · A =⇘β⇙ y⇘β⇙" proof (intro allI impI) fix ℳ and φ assume *: "is_general_model ℳ" "φ ↝⇩_{M}ℳ" show "ℳ ⊨⇘φ⇙ (λx⇘α⇙. y⇘β⇙) · A =⇘β⇙ y⇘β⇙" proof - obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)" using prod_cases3 by blast moreover from assms and * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ ((λx⇘α⇙. y⇘β⇙) · A =⇘β⇙ y⇘β⇙) = ❙T" using general_model.axiom_4_1_var_validity_aux by auto ultimately show ?thesis by simp qed qed lemma (in general_model) axiom_4_2_validity_aux: assumes "φ ↝ 𝒟" and "A ∈ wffs⇘α⇙" shows "𝒱 φ ((λx⇘α⇙. x⇘α⇙) · A =⇘α⇙ A) = ❙T" proof - from assms(2) have "(λx⇘α⇙. x⇘α⇙) · A =⇘α⇙ A ∈ wffs⇘o⇙" using axioms.axiom_4_2 and axioms_are_wffs_of_type_o by blast define ψ where "ψ = φ((x, α) := 𝒱 φ A)" with assms have "𝒱 φ ((λx⇘α⇙. x⇘α⇙) · A) = 𝒱 ψ (x⇘α⇙)" using prop_5401_a by blast also from assms and ψ_def have "… = ψ (x, α)" using 𝒱_is_wff_denotation_function by force also from ψ_def have "… = 𝒱 φ A" by simp finally have "𝒱 φ ((λx⇘α⇙. x⇘α⇙) · A) = 𝒱 φ A" . with assms(1) and ‹(λx⇘α⇙. x⇘α⇙) · A =⇘α⇙ A ∈ wffs⇘o⇙› show ?thesis using wffs_from_equality and prop_5401_b by meson qed lemma axiom_4_2_validity: assumes "A ∈ wffs⇘α⇙" shows "⊨ (λx⇘α⇙. x⇘α⇙) · A =⇘α⇙ A" proof (intro allI impI) fix ℳ and φ assume *: "is_general_model ℳ" "φ ↝⇩_{M}ℳ" show "ℳ ⊨⇘φ⇙ (λx⇘α⇙. x⇘α⇙) · A =⇘α⇙ A" proof - obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)" using prod_cases3 by blast moreover from assms and * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ ((λx⇘α⇙. x⇘α⇙) · A =⇘α⇙ A) = ❙T" using general_model.axiom_4_2_validity_aux by simp ultimately show ?thesis by simp qed qed lemma (in general_model) axiom_4_3_validity_aux: assumes "φ ↝ 𝒟" and "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘γ→β⇙" and "C ∈ wffs⇘γ⇙" shows "𝒱 φ ((λx⇘α⇙. B · C) · A =⇘β⇙ ((λx⇘α⇙. B) · A) · ((λx⇘α⇙. C) · A)) = ❙T" (is "𝒱 φ (?A =⇘β⇙ ?B) = ❙T") proof - from assms(2-4) have "?A =⇘β⇙ ?B ∈ wffs⇘o⇙" using axioms.axiom_4_3 and axioms_are_wffs_of_type_o by blast define ψ where "ψ = φ((x, α) := 𝒱 φ A)" with assms(1,2) have "ψ ↝ 𝒟" using 𝒱_is_wff_denotation_function by auto from assms and ψ_def have "𝒱 φ ?A = 𝒱 ψ (B · C)" using prop_5401_a by blast also from assms(3,4) and ψ_def and ‹ψ ↝ 𝒟› have "… = 𝒱 ψ B ∙ 𝒱 ψ C" using 𝒱_is_wff_denotation_function by blast also from assms(1-3) and ψ_def have "… = 𝒱 φ ((λx⇘α⇙. B) · A) ∙ 𝒱 ψ C" using prop_5401_a by simp also from assms(1,2,4) and ψ_def have "… = 𝒱 φ ((λx⇘α⇙. B) · A) ∙ 𝒱 φ ((λx⇘α⇙. C) · A)" using prop_5401_a by simp also have "… = 𝒱 φ ?B" proof - have "(λx⇘α⇙. B) · A ∈ wffs⇘γ→β⇙" and "(λx⇘α⇙. C) · A ∈ wffs⇘γ⇙" using assms(2-4) by blast+ with assms(1) show ?thesis using wff_app_denotation[OF 𝒱_is_wff_denotation_function] by simp qed finally have "𝒱 φ ?A = 𝒱 φ ?B" . with assms(1) and ‹?A =⇘β⇙ ?B ∈ wffs⇘o⇙› show ?thesis using prop_5401_b and wffs_from_equality by meson qed lemma axiom_4_3_validity: assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘γ→β⇙" and "C ∈ wffs⇘γ⇙" shows "⊨ (λx⇘α⇙. B · C) · A =⇘β⇙ ((λx⇘α⇙. B) · A) · ((λx⇘α⇙. C) · A)" (is "⊨ ?A =⇘β⇙ ?B") proof (intro allI impI) fix ℳ and φ assume *: "is_general_model ℳ" "φ ↝⇩_{M}ℳ" show "ℳ ⊨⇘φ⇙ ?A =⇘β⇙ ?B" proof - obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)" using prod_cases3 by blast moreover from assms and * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ (?A =⇘β⇙ ?B) = ❙T" using general_model.axiom_4_3_validity_aux by simp ultimately show ?thesis by simp qed qed lemma (in general_model) axiom_4_4_validity_aux: assumes "φ ↝ 𝒟" and "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘δ⇙" and "(y, γ) ∉ {(x, α)} ∪ vars A" shows "𝒱 φ ((λx⇘α⇙. λy⇘γ⇙. B) · A =⇘γ→δ⇙ (λy⇘γ⇙. (λx⇘α⇙. B) · A)) = ❙T" (is "𝒱 φ (?A =⇘γ→δ⇙ ?B) = ❙T") proof - from assms(2,3) have "?A =⇘γ→δ⇙ ?B ∈ wffs⇘o⇙" using axioms.axiom_4_4 and axioms_are_wffs_of_type_o by blast let ?D = "λy⇘γ⇙. B" define ψ where "ψ = φ((x, α) := 𝒱 φ A)" from assms(1,2) and ψ_def have "ψ ↝ 𝒟" using 𝒱_is_wff_denotation_function by simp { fix z assume "z ∈ elts (𝒟 γ)" define φ' where "φ' = φ((y, γ) := z)" from assms(1) and ‹z ∈ elts (𝒟 γ)› and φ'_def have "φ' ↝ 𝒟" by simp moreover from φ'_def and assms(4) have "∀v ∈ free_vars A. φ v = φ' v" using free_vars_in_all_vars by auto ultimately have "𝒱 φ A = 𝒱 φ' A" using assms(1,2) and prop_5400 by blast with ψ_def and φ'_def and assms(4) have "φ'((x, α) := 𝒱 φ' A) = ψ((y, γ) := z)" by auto with ‹ψ ↝ 𝒟› and ‹z ∈ elts (𝒟 γ)› and assms(3) have "𝒱 ψ ?D ∙ z = 𝒱 (ψ((y, γ) := z)) B" by (simp add: mixed_beta_conversion) also from ‹φ' ↝ 𝒟› and assms(2,3) have "… = 𝒱 φ' ((λx⇘α⇙. B) · A)" using prop_5401_a and ‹φ'((x, α) := 𝒱 φ' A) = ψ((y, γ) := z)› by simp also from φ'_def and assms(1) and ‹z ∈ elts (𝒟 γ)› and ‹?A =⇘γ→δ⇙ ?B ∈ wffs⇘o⇙› have "… = 𝒱 φ ?B ∙ z" by (metis mixed_beta_conversion wffs_from_abs wffs_from_equality(2)) finally have "𝒱 ψ ?D ∙ z = 𝒱 φ ?B ∙ z" . } note * = this then have "𝒱 ψ ?D = 𝒱 φ ?B" proof - from ‹ψ ↝ 𝒟› and assms(3) have "𝒱 ψ ?D = (❙λz ❙:𝒟 γ❙.𝒱 (ψ((y, γ) := z)) B)" using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by simp moreover from assms(1) have "𝒱 φ ?B = (❙λz ❙:𝒟 γ❙.𝒱 (φ((y, γ) := z)) ((λx⇘α⇙. B) · A))" using wffs_from_abs[OF wffs_from_equality(2)[OF ‹?A =⇘γ→δ⇙ ?B ∈ wffs⇘o⇙›]] and wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by meson ultimately show ?thesis using vlambda_extensionality and * by fastforce qed with assms(1-3) and ψ_def have "𝒱 φ ?A = 𝒱 φ ?B" using prop_5401_a and wffs_of_type_intros(4) by metis with assms(1) show ?thesis using prop_5401_b and wffs_from_equality[OF ‹?A =⇘γ→δ⇙ ?B ∈ wffs⇘o⇙›] by blast qed lemma axiom_4_4_validity: assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘δ⇙" and "(y, γ) ∉ {(x, α)} ∪ vars A" shows "⊨ (λx⇘α⇙. λy⇘γ⇙. B) · A =⇘γ→δ⇙ (λy⇘γ⇙. (λx⇘α⇙. B) · A)" (is "⊨ ?A =⇘γ→δ⇙ ?B") proof (intro allI impI) fix ℳ and φ assume *: "is_general_model ℳ" "φ ↝⇩_{M}ℳ" show "ℳ ⊨⇘φ⇙ ?A =⇘γ→δ⇙ ?B" proof - obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)" using prod_cases3 by blast moreover from assms and * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ (?A =⇘γ→δ⇙ ?B) = ❙T" using general_model.axiom_4_4_validity_aux by blast ultimately show ?thesis by simp qed qed lemma (in general_model) axiom_4_5_validity_aux: assumes "φ ↝ 𝒟" and "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘δ⇙" shows "𝒱 φ ((λx⇘α⇙. λx⇘α⇙. B) · A =⇘α→δ⇙ (λx⇘α⇙. B)) = ❙T" proof - define ψ where "ψ = φ((x, α) := 𝒱 φ A)" from assms have wff: "(λx⇘α⇙. λx⇘α⇙. B) · A =⇘α→δ⇙ (λx⇘α⇙. B) ∈ wffs⇘o⇙" using axioms.axiom_4_5 and axioms_are_wffs_of_type_o by blast with assms(1,2) and ψ_def have "𝒱 φ ((λx⇘α⇙. λx⇘α⇙. B) · A) = 𝒱 ψ (λx⇘α⇙. B)" using prop_5401_a and wffs_from_equality(2) by blast also have "… = 𝒱 φ (λx⇘α⇙. B)" proof - have "(x, α) ∉ free_vars (λx⇘α⇙. B)" by simp with ψ_def have "∀v ∈ free_vars (λx⇘α⇙. B). φ v = ψ v" by simp moreover from ψ_def and assms(1,2) have "ψ ↝ 𝒟" using 𝒱_is_wff_denotation_function by simp moreover from assms(2,3) have "(λx⇘α⇙. B) ∈ wffs⇘α→δ⇙" by fastforce ultimately show ?thesis using assms(1) and prop_5400 by metis qed finally have "𝒱 φ ((λx⇘α⇙. λx⇘α⇙. B) · A) = 𝒱 φ (λx⇘α⇙. B)" . with wff and assms(1) show ?thesis using prop_5401_b and wffs_from_equality by meson qed lemma axiom_4_5_validity: assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘δ⇙" shows "⊨ (λx⇘α⇙. λx⇘α⇙. B) · A =⇘