Theory Soundness
section ‹Soundness›
theory Soundness
imports
Elementary_Logic
Semantics
begin
unbundle no funcset_syntax
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 (𝒟 α')"
and "∀x' α'. (ψ((x, α) := z)) (x', α') ∈ elts (𝒟 α')"
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 = ❙T then ❙T else ❙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
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
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 = ❙T then ❙T else ❙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 = ❙F then ❙F else ❙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 = ❙T then ❙T else ❙F)"
using ‹{x, y} ⊆ elts 𝔹› by auto
also have "… ⟷ ❙T = (if x = ❙T ∧ y = ❙F then ❙F else ❙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 = ❙F then ❙F else ❙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 "𝒱 ψ