Theory Soundness
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 (𝒟 α')"
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 "𝒱 ψ ?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 =⇘α→δ⇙ (λx⇘α⇙. B)"
proof (intro allI impI)
fix ℳ and φ
assume *: "is_general_model ℳ" "φ ↝⇩M ℳ"
show "ℳ ⊨⇘φ⇙ (λx⇘α⇙. λx⇘α⇙. B) · A =⇘α→δ⇙ (λx⇘α⇙. B)"
proof -
obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)"
using prod_cases3 by blast
moreover
from assms and * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ ((λx⇘α⇙. λx⇘α⇙. B) · A =⇘α→δ⇙ (λx⇘α⇙. B)) = ❙T"
using general_model.axiom_4_5_validity_aux by blast
ultimately show ?thesis
by simp
qed
qed
lemma (in general_model) axiom_5_validity_aux:
assumes "φ ↝ 𝒟"
shows "𝒱 φ (ι · (Q⇘i⇙ · 𝔶⇘i⇙) =⇘i⇙ 𝔶⇘i⇙) = ❙T"
proof -
have "ι · (Q⇘i⇙ · 𝔶⇘i⇙) =⇘i⇙ 𝔶⇘i⇙ ∈ wffs⇘o⇙"
using axioms.axiom_5 and axioms_are_wffs_of_type_o by blast
have "Q⇘i⇙ · 𝔶⇘i⇙ ∈ wffs⇘i→o⇙"
by blast
with assms have "𝒱 φ (ι · (Q⇘i⇙ · 𝔶⇘i⇙)) = 𝒱 φ ι ∙ 𝒱 φ (Q⇘i⇙ · 𝔶⇘i⇙)"
using 𝒱_is_wff_denotation_function by blast
also from assms have "… = 𝒱 φ ι ∙ (𝒱 φ (Q⇘i⇙) ∙ 𝒱 φ (𝔶⇘i⇙))"
using wff_app_denotation[OF 𝒱_is_wff_denotation_function] by (metis Q_wff wffs_of_type_intros(1))
also from assms have "… = 𝒥 (𝔠⇩ι, (i→o)→i) ∙ (𝒥 (𝔠⇩Q, i→i→o) ∙ 𝒱 φ (𝔶⇘i⇙))"
using 𝒱_is_wff_denotation_function by auto
also from assms have "… = 𝒥 (𝔠⇩ι, (i→o)→i) ∙ ((q⇘i⇙⇗𝒟⇖) ∙ 𝒱 φ (𝔶⇘i⇙))"
using Q_constant_of_type_def and Q_denotation by simp
also from assms have "… = 𝒥 (𝔠⇩ι, (i→o)→i) ∙ {𝒱 φ (𝔶⇘i⇙)}⇘i⇙⇗𝒟⇖"
using 𝒱_is_wff_denotation_function by auto
finally have "𝒱 φ (ι · (Q⇘i⇙ · 𝔶⇘i⇙)) = 𝒥 (𝔠⇩ι, (i→o)→i) ∙ {𝒱 φ (𝔶⇘i⇙)}⇘i⇙⇗𝒟⇖" .
moreover from assms have "𝒥 (𝔠⇩ι, (i→o)→i) ∙ {𝒱 φ (𝔶⇘i⇙)}⇘i⇙⇗𝒟⇖ = 𝒱 φ (𝔶⇘i⇙)"
using 𝒱_is_wff_denotation_function and ι_denotation by force
ultimately have "𝒱 φ (ι · (Q⇘i⇙ · 𝔶⇘i⇙)) = 𝒱 φ (𝔶⇘i⇙)"
by (simp only:)
with assms and ‹Q⇘i⇙ · 𝔶⇘i⇙ ∈ wffs⇘i→o⇙› show ?thesis
using prop_5401_b by blast
qed
lemma axiom_5_validity:
shows "⊨ ι · (Q⇘i⇙ · 𝔶⇘i⇙) =⇘i⇙ 𝔶⇘i⇙"
proof (intro allI impI)
fix ℳ and φ
assume *: "is_general_model ℳ" "φ ↝⇩M ℳ"
show "ℳ ⊨⇘φ⇙ ι · (Q⇘i⇙ · 𝔶⇘i⇙) =⇘i⇙ 𝔶⇘i⇙"
proof -
obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)"
using prod_cases3 by blast
moreover from * and ‹ℳ = (𝒟, 𝒥, 𝒱)› have "𝒱 φ (ι · (Q⇘i⇙ · 𝔶⇘i⇙) =⇘i⇙ 𝔶⇘i⇙) = ❙T"
using general_model.axiom_5_validity_aux by simp
ultimately show ?thesis
by simp
qed
qed
lemma axioms_validity:
assumes "A ∈ axioms"
shows "⊨ A"
using assms
and axiom_1_validity
and axiom_2_validity
and axiom_3_validity
and axiom_4_1_con_validity
and axiom_4_1_var_validity
and axiom_4_2_validity
and axiom_4_3_validity
and axiom_4_4_validity
and axiom_4_5_validity
and axiom_5_validity
by cases auto
lemma (in general_model) rule_R_validity_aux:
assumes "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙"
and "∀φ. φ ↝ 𝒟 ⟶ 𝒱 φ A = 𝒱 φ B"
and "C ∈ wffs⇘β⇙" and "C' ∈ wffs⇘β⇙"
and "p ∈ positions C" and "A ≼⇘p⇙ C" and "C⦉p ← B⦊ ⊳ C'"
shows "∀φ. φ ↝ 𝒟 ⟶ 𝒱 φ C = 𝒱 φ C'"
proof -
from assms(8,3-5,7) show ?thesis
proof (induction arbitrary: β)
case pos_found
then show ?case
by simp
next
case (replace_left_app p G B' G' H)
show ?case
proof (intro allI impI)
fix φ
assume "φ ↝ 𝒟"
from ‹G · H ∈ wffs⇘β⇙› obtain γ where "G ∈ wffs⇘γ→β⇙" and "H ∈ wffs⇘γ⇙"
by (rule wffs_from_app)
with ‹G' · H ∈ wffs⇘β⇙› have "G' ∈ wffs⇘γ→β⇙"
by (metis wff_has_unique_type wffs_from_app)
from assms(1) and ‹φ ↝ 𝒟› and ‹G ∈ wffs⇘γ→β⇙› and ‹H ∈ wffs⇘γ⇙›
have "𝒱 φ (G · H) = 𝒱 φ G ∙ 𝒱 φ H"
using 𝒱_is_wff_denotation_function by blast
also from ‹φ ↝ 𝒟› and ‹G ∈ wffs⇘γ→β⇙› and ‹G' ∈ wffs⇘γ→β⇙› have "… = 𝒱 φ G' ∙ 𝒱 φ H"
using replace_left_app.IH and replace_left_app.prems(1,4) by simp
also from assms(1) and ‹φ ↝ 𝒟› and ‹G' ∈ wffs⇘γ→β⇙› and ‹H ∈ wffs⇘γ⇙›
have "… = 𝒱 φ (G' · H)"
using 𝒱_is_wff_denotation_function by fastforce
finally show "𝒱 φ (G · H) = 𝒱 φ (G' · H)" .
qed
next
case (replace_right_app p H B' H' G)
show ?case
proof (intro allI impI)
fix φ
assume "φ ↝ 𝒟"
from ‹G · H ∈ wffs⇘β⇙› obtain γ where "G ∈ wffs⇘γ→β⇙" and "H ∈ wffs⇘γ⇙"
by (rule wffs_from_app)
with ‹G · H' ∈ wffs⇘β⇙› have "H' ∈ wffs⇘γ⇙"
using wff_has_unique_type and wffs_from_app by (metis type.inject)
from assms(1) and ‹φ ↝ 𝒟› and ‹G ∈ wffs⇘γ→β⇙› and ‹H ∈ wffs⇘γ⇙›
have "𝒱 φ (G · H) = 𝒱 φ G ∙ 𝒱 φ H"
using 𝒱_is_wff_denotation_function by blast
also from ‹φ ↝ 𝒟› and ‹H ∈ wffs⇘γ⇙› and ‹H' ∈ wffs⇘γ⇙› have "… = 𝒱 φ G ∙ 𝒱 φ H'"
using replace_right_app.IH and replace_right_app.prems(1,4) by force
also from assms(1) and ‹φ ↝ 𝒟› and ‹G ∈ wffs⇘γ→β⇙› and ‹H' ∈ wffs⇘γ⇙›
have "… = 𝒱 φ (G · H')"
using 𝒱_is_wff_denotation_function by fastforce
finally show "𝒱 φ (G · H) = 𝒱 φ (G · H')" .
qed
next
case (replace_abs p E B' E' x γ)
show ?case
proof (intro allI impI)
fix φ
assume "φ ↝ 𝒟"
define ψ where "ψ z = φ((x, γ) := z)" for z
with ‹φ ↝ 𝒟› have ψ_assg: "ψ z ↝ 𝒟" if "z ∈ elts (𝒟 γ)" for z
by (simp add: that)
from ‹λx⇘γ⇙. E ∈ wffs⇘β⇙› obtain δ where "β = γ→δ" and "E ∈ wffs⇘δ⇙"
by (rule wffs_from_abs)
with ‹λx⇘γ⇙. E' ∈ wffs⇘β⇙› have "E' ∈ wffs⇘δ⇙"
using wffs_from_abs by blast
from assms(1) and ‹φ ↝ 𝒟› and ‹E ∈ wffs⇘δ⇙› and ψ_def
have "𝒱 φ (λx⇘γ⇙. E) = (❙λz ❙: 𝒟 γ❙. 𝒱 (ψ z) E)"
using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by simp
also have "… = (❙λz ❙: 𝒟 γ❙. 𝒱 (ψ z) E')"
proof (intro vlambda_extensionality)
fix z
assume "z ∈ elts (𝒟 γ)"
from ‹E ∈ wffs⇘δ⇙› and ‹E' ∈ wffs⇘δ⇙› have "∀φ. φ ↝ 𝒟 ⟶ 𝒱 φ E = 𝒱 φ E'"
using replace_abs.prems(1,4) and replace_abs.IH by simp
with ψ_assg and ‹z ∈ elts (𝒟 γ)› show "𝒱 (ψ z) E = 𝒱 (ψ z) E'"
by simp
qed
also from assms(1) and ‹φ ↝ 𝒟› and ‹E' ∈ wffs⇘δ⇙› and ψ_def
have "… = 𝒱 φ (λx⇘γ⇙. E')"
using wff_abs_denotation[OF 𝒱_is_wff_denotation_function] by simp
finally show "𝒱 φ (λx⇘γ⇙. E) = 𝒱 φ (λx⇘γ⇙. E')" .
qed
qed
qed
lemma rule_R_validity:
assumes "C ∈ wffs⇘o⇙" and "C' ∈ wffs⇘o⇙" and "E ∈ wffs⇘o⇙"
and "⊨ C" and "⊨ E"
and "is_rule_R_app p C' C E"
shows "⊨ C'"
proof (intro allI impI)
fix ℳ and φ
assume "is_general_model ℳ" and "φ ↝⇩M ℳ"
show "ℳ ⊨⇘φ⇙ C'"
proof -
have "ℳ ⊨ C'"
proof -
obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)"
using prod_cases3 by blast
from assms(6) obtain A and B and α where "A ∈ wffs⇘α⇙" and "B ∈ wffs⇘α⇙" and "E = A =⇘α⇙ B"
using wffs_from_equality by (meson is_rule_R_app_def)
note * = ‹is_general_model ℳ› ‹ℳ = (𝒟, 𝒥, 𝒱)› ‹φ ↝⇩M ℳ›
have "𝒱 φ' C = 𝒱 φ' C'" if "φ' ↝ 𝒟" for φ'
proof -
from assms(5) and *(1,2) and ‹A ∈ wffs⇘α⇙› and ‹B ∈ wffs⇘α⇙› and ‹E = A =⇘α⇙ B› and that
have "∀φ'. φ' ↝ 𝒟 ⟶𝒱 φ' A = 𝒱 φ' B"
using general_model.prop_5401_b by blast
moreover
from ‹E = A =⇘α⇙ B› and assms(6) have "p ∈ positions C" and "A ≼⇘p⇙ C" and "C⦉p ← B⦊ ⊳ C'"
using is_subform_implies_in_positions by auto
ultimately show ?thesis
using ‹A ∈ wffs⇘α⇙› and ‹B ∈ wffs⇘α⇙› and ‹C ∈ wffs⇘o⇙› and assms(2) and that and *(1,2)
and general_model.rule_R_validity_aux by blast
qed
with assms(4) and *(1,2) show ?thesis
by simp
qed
with ‹φ ↝⇩M ℳ› show ?thesis
by blast
qed
qed
lemma individual_proof_step_validity:
assumes "is_proof 𝒮" and "A ∈ lset 𝒮"
shows "⊨ A"
using assms proof (induction "length 𝒮" arbitrary: 𝒮 A rule: less_induct)
case less
from ‹A ∈ lset 𝒮› obtain i' where "𝒮 ! i' = A" and "𝒮 ≠ []" and "i' < length 𝒮"
by (metis empty_iff empty_set in_set_conv_nth)
with ‹is_proof 𝒮› have "is_proof (take (Suc i') 𝒮)" and "take (Suc i') 𝒮 ≠ []"
using proof_prefix_is_proof[where 𝒮⇩1 = "take (Suc i') 𝒮" and 𝒮⇩2 = "drop (Suc i') 𝒮"]
and append_take_drop_id by simp_all
from ‹i' < length 𝒮› consider (a) "i' < length 𝒮 - 1" | (b) "i' = length 𝒮 - 1"
by fastforce
then show ?case
proof cases
case a
then have "length (take (Suc i') 𝒮) < length 𝒮"
by simp
with ‹𝒮 ! i' = A› and ‹take (Suc i') 𝒮 ≠ []› have "A ∈ lset (take (Suc i') 𝒮)"
by (simp add: take_Suc_conv_app_nth)
with ‹length (take (Suc i') 𝒮) < length 𝒮› and ‹is_proof (take (Suc i') 𝒮)› show ?thesis
using less(1) by blast
next
case b
with ‹𝒮 ! i' = A› and ‹𝒮 ≠ []› have "last 𝒮 = A"
using last_conv_nth by blast
with ‹is_proof 𝒮› and ‹𝒮 ≠ []› and b have "is_proof_step 𝒮 i'"
using added_suffix_proof_preservation[where 𝒮' = "[]"] by simp
then consider
(axiom) "𝒮 ! i' ∈ axioms"
| (rule_R) "∃p j k. {j, k} ⊆ {0..<i'} ∧ is_rule_R_app p (𝒮 ! i') (𝒮 ! j) (𝒮 ! k)"
by fastforce
then show ?thesis
proof cases
case axiom
with ‹𝒮 ! i' = A› show ?thesis
by (blast dest: axioms_validity)
next
case rule_R
then obtain p and j and k
where "{j, k} ⊆ {0..<i'}" and "is_rule_R_app p (𝒮 ! i') (𝒮 ! j) (𝒮 ! k)"
by blast
let ?𝒮⇩j = "take (Suc j) 𝒮" and ?𝒮⇩k = "take (Suc k) 𝒮"
obtain 𝒮⇩j' and 𝒮⇩k' where "𝒮 = ?𝒮⇩j @ 𝒮⇩j'" and "𝒮 = ?𝒮⇩k @ 𝒮⇩k'"
by (metis append_take_drop_id)
with ‹is_proof 𝒮› have "is_proof (?𝒮⇩j @ 𝒮⇩j')" and "is_proof (?𝒮⇩k @ 𝒮⇩k')"
by (simp_all only:)
moreover from ‹𝒮 ≠ []› have "?𝒮⇩j ≠ []" and "?𝒮⇩k ≠ []"
by simp_all
ultimately have "is_proof_of ?𝒮⇩j (last ?𝒮⇩j)" and "is_proof_of ?𝒮⇩k (last ?𝒮⇩k)"
using proof_prefix_is_proof_of_last[where 𝒮 = ?𝒮⇩j and 𝒮' = 𝒮⇩j']
and proof_prefix_is_proof_of_last[where 𝒮 = ?𝒮⇩k and 𝒮' = 𝒮⇩k']
by fastforce+
moreover
from ‹{j, k} ⊆ {0..<i'}› and b have "length ?𝒮⇩j < length 𝒮" and "length ?𝒮⇩k < length 𝒮"
by force+
moreover from calculation(3,4) have "𝒮 ! j ∈ lset ?𝒮⇩j" and "𝒮 ! k ∈ lset ?𝒮⇩k"
by (simp_all add: take_Suc_conv_app_nth)
ultimately have "⊨ 𝒮 ! j" and "⊨ 𝒮 ! k"
using ‹?𝒮⇩j ≠ []› and ‹?𝒮⇩k ≠ []› and less(1) unfolding is_proof_of_def by presburger+
moreover have "𝒮 ! i' ∈ wffs⇘o⇙" and "𝒮 ! j ∈ wffs⇘o⇙" and "𝒮 ! k ∈ wffs⇘o⇙"
using ‹is_rule_R_app p (𝒮 ! i') (𝒮 ! j) (𝒮 ! k)› and replacement_preserves_typing
by force+
ultimately show ?thesis
using ‹is_rule_R_app p (𝒮 ! i') (𝒮 ! j) (𝒮 ! k)› and ‹𝒮 ! i' = A›
and rule_R_validity[where C' = A] by blast
qed
qed
qed
lemma semantic_modus_ponens:
assumes "is_general_model ℳ"
and "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
and "ℳ ⊨ A ⊃⇧𝒬 B"
and "ℳ ⊨ A"
shows "ℳ ⊨ B"
proof (intro allI impI)
fix φ
assume "φ ↝⇩M ℳ"
moreover obtain 𝒟 and 𝒥 and 𝒱 where "ℳ = (𝒟, 𝒥, 𝒱)"
using prod_cases3 by blast
ultimately have "φ ↝ 𝒟"
by simp
show "ℳ ⊨⇘φ⇙ B"
proof -
from assms(4) have "𝒱 φ (A ⊃⇧𝒬 B) = ❙T"
using ‹ℳ = (𝒟, 𝒥, 𝒱)› and ‹φ ↝⇩M ℳ› by auto
with assms(1-3) have "𝒱 φ A ❙⊃ 𝒱 φ B = ❙T"
using ‹ℳ = (𝒟, 𝒥, 𝒱)› and ‹φ ↝⇩M ℳ› and general_model.prop_5401_f' by simp
moreover from assms(5) have "𝒱 φ A = ❙T"
using ‹ℳ = (𝒟, 𝒥, 𝒱)› and ‹φ ↝ 𝒟› by auto
moreover from ‹ℳ = (𝒟, 𝒥, 𝒱)› and assms(1) have "elts (𝒟 o) = elts 𝔹"
using frame.truth_values_domain_def and general_model_def and premodel_def by fastforce
with assms and ‹ℳ = (𝒟, 𝒥, 𝒱)› and ‹φ ↝ 𝒟› and ‹𝒱 φ A = ❙T› have "{𝒱 φ A, 𝒱 φ B} ⊆ elts 𝔹"
using general_model.𝒱_is_wff_denotation_function
and premodel.wff_denotation_function_is_domain_respecting and general_model.axioms(1) by blast
ultimately have "𝒱 φ B = ❙T"
by fastforce
with ‹ℳ = (𝒟, 𝒥, 𝒱)› and assms(1) and ‹φ ↝ 𝒟› show ?thesis
by simp
qed
qed
lemma generalized_semantic_modus_ponens:
assumes "is_general_model ℳ"
and "lset hs ⊆ wffs⇘o⇙"
and "∀H ∈ lset hs. ℳ ⊨ H"
and "P ∈ wffs⇘o⇙"
and "ℳ ⊨ hs ⊃⇧𝒬⇩⋆ P"
shows "ℳ ⊨ P"
using assms(2-5) proof (induction hs arbitrary: P rule: rev_induct)
case Nil
then show ?case by simp
next
case (snoc H' hs)
from ‹ℳ ⊨ (hs @ [H']) ⊃⇧𝒬⇩⋆ P› have "ℳ ⊨ hs ⊃⇧𝒬⇩⋆ (H' ⊃⇧𝒬 P)"
by simp
moreover from ‹∀H ∈ lset (hs @ [H']). ℳ ⊨ H› and ‹lset (hs @ [H']) ⊆ wffs⇘o⇙›
have "∀H ∈ lset hs. ℳ ⊨ H" and "lset hs ⊆ wffs⇘o⇙"
by simp_all
moreover from ‹lset (hs @ [H']) ⊆ wffs⇘o⇙› and ‹P ∈ wffs⇘o⇙› have "H' ⊃⇧𝒬 P ∈ wffs⇘o⇙"
by auto
ultimately have "ℳ ⊨ H' ⊃⇧𝒬 P"
by (elim snoc.IH)
moreover from ‹∀H ∈ lset (hs @ [H']). ℳ ⊨ H› have "ℳ ⊨ H'"
by simp
moreover from ‹H' ⊃⇧𝒬 P ∈ wffs⇘o⇙› have "H' ∈ wffs⇘o⇙"
using wffs_from_imp_op(1) by blast
ultimately show ?case
using assms(1) and ‹P ∈ wffs⇘o⇙› and semantic_modus_ponens by simp
qed
subsection ‹Proposition 5402(a)›
proposition theoremhood_implies_validity:
assumes "is_theorem A"
shows "⊨ A"
using assms and individual_proof_step_validity by force
subsection ‹Proposition 5402(b)›
proposition hyp_derivability_implies_validity:
assumes "is_hyps 𝒢"
and "is_model_for ℳ 𝒢"
and "𝒢 ⊢ A"
and "is_general_model ℳ"
shows "ℳ ⊨ A"
proof -
from assms(3) have "A ∈ wffs⇘o⇙"
by (fact hyp_derivable_form_is_wffso)
from ‹𝒢 ⊢ A› and ‹is_hyps 𝒢› obtain ℋ where "finite ℋ" and "ℋ ⊆ 𝒢" and "ℋ ⊢ A"
by blast
moreover from ‹finite ℋ› obtain hs where "lset hs = ℋ"
using finite_list by blast
ultimately have "⊢ hs ⊃⇧𝒬⇩⋆ A"
using generalized_deduction_theorem by simp
with assms(4) have "ℳ ⊨ hs ⊃⇧𝒬⇩⋆ A"
using derivability_from_no_hyps_theoremhood_equivalence and theoremhood_implies_validity
by blast
moreover from ‹ℋ ⊆ 𝒢› and assms(2) have "ℳ ⊨ H" if "H ∈ ℋ" for H
using that by blast
moreover from ‹ℋ ⊆ 𝒢› and ‹lset hs = ℋ› and assms(1) have "lset hs ⊆ wffs⇘o⇙"
by blast
ultimately show ?thesis
using assms(1,4) and ‹A ∈ wffs⇘o⇙› and ‹lset hs = ℋ› and generalized_semantic_modus_ponens
by auto
qed
subsection ‹Theorem 5402 (Soundness Theorem)›
lemmas thm_5402 = theoremhood_implies_validity hyp_derivability_implies_validity
end