Theory Semantics

section ‹Semantics›

theory Semantics
  imports
    "ZFC_in_HOL.ZFC_Typeclasses"
    Syntax
    Boolean_Algebra
begin

no_notation funcset (infixr "→" 60)
notation funcset (infixr "⇸" 60)

abbreviation vfuncset :: "V ⇒ V ⇒ V" (infixr "⟼" 60) where
  "A ⟼ B ≡ VPi A (λ_. B)"

notation app (infixl "∙" 300)

syntax
  "_vlambda" :: "pttrn ⇒ V ⇒ (V ⇒ V) ⇒ V" ("(3❙λ_❙:_ ❙./ _)" [0, 0, 3] 3)
translations
  "❙λx ❙: A❙. f" ⇌ "CONST VLambda A (λx. f)"

lemma vlambda_extensionality:
  assumes "⋀x. x ∈ elts A ⟹ f x = g x"
  shows "(❙λx ❙: A❙. f x) = (❙λx ❙: A❙. g x)"
  unfolding VLambda_def using assms by auto

subsection ‹Frames›

locale frame =
  fixes 𝒟 :: "type ⇒ V"
  assumes truth_values_domain_def: "𝒟 o = 𝔹"
  and function_domain_def: "∀α β. 𝒟 (α→β) ≤ 𝒟 α ⟼ 𝒟 β"
  and domain_nonemptiness: "∀α. 𝒟 α ≠ 0"
begin

lemma function_domainD:
  assumes "f ∈ elts (𝒟 (α→β))"
  shows "f ∈ elts (𝒟 α ⟼ 𝒟 β)"
  using assms and function_domain_def by blast

lemma vlambda_from_function_domain:
  assumes "f ∈ elts (𝒟 (α→β))"
  obtains b where "f = (❙λx ❙: 𝒟 α❙. b x)" and "∀x ∈ elts (𝒟 α). b x ∈ elts (𝒟 β)"
  using function_domainD[OF assms] by (metis VPi_D eta)

lemma app_is_domain_respecting:
  assumes "f ∈ elts (𝒟 (α→β))" and "x ∈ elts (𝒟 α)"
  shows "f ∙ x ∈ elts (𝒟 β)"
  by (fact VPi_D[OF function_domainD[OF assms(1)] assms(2)])

text ‹One-element function on @{term ‹𝒟 α›}:›

definition one_element_function :: "V ⇒ type ⇒ V" ("{_}⇘_⇙" [901, 0] 900) where
  [simp]: "{x}⇘α⇙ = (❙λy ❙: 𝒟 α❙. bool_to_V (y = x))"

lemma one_element_function_is_domain_respecting:
  shows "{x}⇘α⇙ ∈ elts (𝒟 α ⟼ 𝒟 o)"
  unfolding one_element_function_def and truth_values_domain_def by (intro VPi_I) (simp, metis)

lemma one_element_function_simps:
  shows "x ∈ elts (𝒟 α) ⟹ {x}⇘α⇙ ∙ x = ❙T"
  and "⟦{x, y} ⊆ elts (𝒟 α); y ≠ x⟧ ⟹ {x}⇘α⇙ ∙ y = ❙F"
  by simp_all

lemma one_element_function_injectivity:
  assumes "{x, x'} ⊆ elts (𝒟 i)" and "{x}⇘i⇙ = {x'}⇘i⇙"
  shows "x = x'"
  using assms(1) and VLambda_eq_D2[OF assms(2)[unfolded one_element_function_def]]
  and injD[OF bool_to_V_injectivity] by blast

lemma one_element_function_uniqueness:
  assumes "x ∈ elts (𝒟 i)"
  shows "(SOME x'. x' ∈ elts (𝒟 i) ∧ {x}⇘i⇙ = {x'}⇘i⇙) = x"
  by (auto simp add: assms one_element_function_injectivity)

text ‹Identity relation on @{term ‹𝒟 α›}:›

definition identity_relation :: "type ⇒ V" ("q⇘_⇙" [0] 100) where
  [simp]: "q⇘α⇙ = (❙λx ❙: 𝒟 α❙. {x}⇘α⇙)"

lemma identity_relation_is_domain_respecting:
  shows "q⇘α⇙ ∈ elts (𝒟 α ⟼ 𝒟 α ⟼ 𝒟 o)"
  using VPi_I and one_element_function_is_domain_respecting by simp

lemma q_is_equality:
  assumes "{x, y} ⊆ elts (𝒟 α)"
  shows "(q⇘α⇙) ∙ x ∙ y = ❙T ⟷ x = y"
  unfolding identity_relation_def
  using assms and injD[OF bool_to_V_injectivity] by fastforce

text ‹Unique member selector:›

definition is_unique_member_selector :: "V ⇒ bool" where
  [iff]: "is_unique_member_selector f ⟷ (∀x ∈ elts (𝒟 i). f ∙ {x}⇘i⇙ = x)"

text ‹Assignment:›

definition is_assignment :: "(var ⇒ V) ⇒ bool" where
  [iff]: "is_assignment φ ⟷ (∀x α. φ (x, α) ∈ elts (𝒟 α))"

end

abbreviation one_element_function_in ("{_}⇘_⇙⇗_⇖" [901, 0, 0] 900) where
  "{x}⇘α⇙⇗𝒟⇖ ≡ frame.one_element_function 𝒟 x α"

abbreviation identity_relation_in ("q⇘_⇙⇗_⇖" [0, 0] 100) where
  "q⇘α⇙⇗𝒟⇖ ≡ frame.identity_relation 𝒟 α"

text ‹
  ‹ψ› is a ``‹v›-variant'' of ‹φ› if ‹ψ› is an assignment that agrees with ‹φ› except possibly on
  ‹v›:
›

definition is_variant_of :: "(var ⇒ V) ⇒ var ⇒ (var ⇒ V) ⇒ bool" ("_ ∼⇘_⇙ _" [51, 0, 51] 50) where
  [iff]: "ψ ∼⇘v⇙ φ ⟷ (∀v'. v' ≠ v ⟶ ψ v' = φ v')"

subsection ‹Pre-models (interpretations)›

text ‹We use the term ``pre-model'' instead of ``interpretation'' since the latter is already a keyword:›

locale premodel = frame +
  fixes 𝒥 :: "con ⇒ V"
  assumes Q_denotation: "∀α. 𝒥 (Q_constant_of_type α) = q⇘α⇙"
  and ι_denotation: "is_unique_member_selector (𝒥 iota_constant)"
  and non_logical_constant_denotation: "∀c α. ¬ is_logical_constant (c, α) ⟶ 𝒥 (c, α) ∈ elts (𝒟 α)"
begin

text ‹Wff denotation function:›

definition is_wff_denotation_function :: "((var ⇒ V) ⇒ form ⇒ V) ⇒ bool" where
  [iff]: "is_wff_denotation_function 𝒱 ⟷
    (
      ∀φ. is_assignment φ ⟶
        (∀A α. A ∈ wffs⇘α⇙ ⟶ 𝒱 φ A ∈ elts (𝒟 α)) ∧ ― ‹closure condition, see note in page 186›
        (∀x α. 𝒱 φ (x⇘α⇙) = φ (x, α)) ∧
        (∀c α. 𝒱 φ (⦃c⦄⇘α⇙) = 𝒥 (c, α)) ∧
        (∀A B α β. A ∈ wffs⇘β→α⇙ ∧ B ∈ wffs⇘β⇙ ⟶ 𝒱 φ (A · B) = (𝒱 φ A) ∙ (𝒱 φ B)) ∧
        (∀x B α β. B ∈ wffs⇘β⇙ ⟶ 𝒱 φ (λx⇘α⇙. B) = (❙λz ❙: 𝒟 α❙. 𝒱 (φ((x, α) := z)) B))
    )"

lemma wff_denotation_function_is_domain_respecting:
  assumes "is_wff_denotation_function 𝒱"
  and "A ∈ wffs⇘α⇙"
  and "is_assignment φ"
  shows "𝒱 φ A ∈ elts (𝒟 α)"
  using assms by force

lemma wff_var_denotation:
  assumes "is_wff_denotation_function 𝒱"
  and "is_assignment φ"
  shows "𝒱 φ (x⇘α⇙) = φ (x, α)"
  using assms by force

lemma wff_Q_denotation:
  assumes "is_wff_denotation_function 𝒱"
  and "is_assignment φ"
  shows "𝒱 φ (Q⇘α⇙) = q⇘α⇙"
  using assms and Q_denotation by force

lemma wff_iota_denotation:
  assumes "is_wff_denotation_function 𝒱"
  and "is_assignment φ"
  shows "is_unique_member_selector (𝒱 φ ι)"
  using assms and ι_denotation by fastforce

lemma wff_non_logical_constant_denotation:
  assumes "is_wff_denotation_function 𝒱"
  and "is_assignment φ"
  and "¬ is_logical_constant (c, α)"
  shows "𝒱 φ (⦃c⦄⇘α⇙) = 𝒥 (c, α)"
  using assms by auto

lemma wff_app_denotation:
  assumes "is_wff_denotation_function 𝒱"
  and "is_assignment φ"
  and "A ∈ wffs⇘β→α⇙"
  and "B ∈ wffs⇘β⇙"
  shows "𝒱 φ (A · B) = 𝒱 φ A ∙ 𝒱 φ B"
  using assms by blast

lemma wff_abs_denotation:
  assumes "is_wff_denotation_function 𝒱"
  and "is_assignment φ"
  and "B ∈ wffs⇘β⇙"
  shows "𝒱 φ (λx⇘α⇙. B) = (❙λz ❙: 𝒟 α❙. 𝒱 (φ((x, α) := z)) B)"
  using assms unfolding is_wff_denotation_function_def by metis

lemma wff_denotation_function_is_uniquely_determined:
  assumes "is_wff_denotation_function 𝒱"
  and "is_wff_denotation_function 𝒱'"
  and "is_assignment φ"
  and "A ∈ wffs"
  shows "𝒱 φ A = 𝒱' φ A"
proof -
  obtain α where "A ∈ wffs⇘α⇙"
    using assms(4) by blast
  then show ?thesis
  using assms(3) proof (induction A arbitrary: φ)
    case var_is_wff
    with assms(1,2) show ?case
      by auto
  next
    case con_is_wff
    with assms(1,2) show ?case
      by auto
  next
    case app_is_wff
    with assms(1,2) show ?case
      using wff_app_denotation by metis
  next
    case (abs_is_wff β A α x)
    have "is_assignment (φ((x, α) := z))" if "z ∈ elts (𝒟 α)" for z
      using that and abs_is_wff.prems by simp
    then have *: "𝒱 (φ((x, α) := z)) A = 𝒱' (φ((x, α) := z)) A" if "z ∈ elts (𝒟 α)" for z
      using abs_is_wff.IH and that by blast
    have "𝒱 φ (λx⇘α⇙. A) = (❙λz ❙: 𝒟 α❙. 𝒱 (φ((x, α) := z)) A)"
      by (fact wff_abs_denotation[OF assms(1) abs_is_wff.prems abs_is_wff.hyps])
    also have "… = (❙λz ❙: 𝒟 α❙. 𝒱' (φ((x, α) := z)) A)"
      using * and vlambda_extensionality by fastforce
    also have "… = 𝒱' φ (λx⇘α⇙. A)"
      by (fact wff_abs_denotation[OF assms(2) abs_is_wff.prems abs_is_wff.hyps, symmetric])
    finally show ?case .
  qed
qed

end

subsection ‹General models›

type_synonym model_structure = "(type ⇒ V) × (con ⇒ V) × ((var ⇒ V) ⇒ form ⇒ V)"

text ‹
  The assumption in the following locale implies that there must exist a function that is a wff
  denotation function for the pre-model, which is a requirement in the definition of general model
  in \<^cite>‹"andrews:2002"›:
›

locale general_model = premodel +
  fixes 𝒱 :: "(var ⇒ V) ⇒ form ⇒ V"
  assumes 𝒱_is_wff_denotation_function: "is_wff_denotation_function 𝒱"
begin

lemma mixed_beta_conversion:
  assumes "is_assignment φ"
  and "y ∈ elts (𝒟 α)"
  and "B ∈ wffs⇘β⇙"
  shows "𝒱 φ (λx⇘α⇙. B) ∙ y = 𝒱 (φ((x, α) := y)) B"
  using wff_abs_denotation[OF 𝒱_is_wff_denotation_function assms(1,3)] and beta[OF assms(2)] by simp

lemma conj_fun_is_domain_respecting:
  assumes "is_assignment φ"
  shows "𝒱 φ (∧⇘o→o→o⇙) ∈ elts (𝒟 (o→o→o))"
  using assms and conj_fun_wff and 𝒱_is_wff_denotation_function by auto

lemma fully_applied_conj_fun_is_domain_respecting:
  assumes "is_assignment φ"
  and "{x, y} ⊆ elts (𝒟 o)"
  shows "𝒱 φ (∧⇘o→o→o⇙) ∙ x ∙ y ∈ elts (𝒟 o)"
  using assms and conj_fun_is_domain_respecting and app_is_domain_respecting by (meson insert_subset)

lemma imp_fun_denotation_is_domain_respecting:
  assumes "is_assignment φ"
  shows "𝒱 φ (⊃⇘o→o→o⇙) ∈ elts (𝒟 (o→o→o))"
  using assms and imp_fun_wff and 𝒱_is_wff_denotation_function by simp

lemma fully_applied_imp_fun_denotation_is_domain_respecting:
  assumes "is_assignment φ"
  and "{x, y} ⊆ elts (𝒟 o)"
  shows "𝒱 φ (⊃⇘o→o→o⇙) ∙ x ∙ y ∈ elts (𝒟 o)"
  using assms and imp_fun_denotation_is_domain_respecting and app_is_domain_respecting
  by (meson insert_subset)

end

abbreviation is_general_model :: "model_structure ⇒ bool" where
  "is_general_model ℳ ≡ case ℳ of (𝒟, 𝒥, 𝒱) ⇒ general_model 𝒟 𝒥 𝒱"

subsection ‹Standard models›

locale standard_model = general_model +
  assumes full_function_domain_def: "∀α β. 𝒟 (α→β) = 𝒟 α ⟼ 𝒟 β"

abbreviation is_standard_model :: "model_structure ⇒ bool" where
  "is_standard_model ℳ ≡ case ℳ of (𝒟, 𝒥, 𝒱) ⇒ standard_model 𝒟 𝒥 𝒱"

lemma standard_model_is_general_model:
  assumes "is_standard_model ℳ"
  shows "is_general_model ℳ"
  using assms and standard_model.axioms(1) by force

subsection ‹Validity›

abbreviation is_assignment_into_frame ("_ ↝ _" [51, 51] 50) where
  "φ ↝ 𝒟 ≡ frame.is_assignment 𝒟 φ"

abbreviation is_assignment_into_model ("_ ↝⇩M _" [51, 51] 50) where
  "φ ↝⇩M ℳ ≡ (case ℳ of (𝒟, 𝒥, 𝒱) ⇒ φ ↝ 𝒟)"

abbreviation satisfies ("_ ⊨⇘_⇙ _" [50, 50, 50] 50) where
  "ℳ ⊨⇘φ⇙ A ≡ case ℳ of (𝒟, 𝒥, 𝒱) ⇒ 𝒱 φ A = ❙T"

abbreviation is_satisfiable_in where
  "is_satisfiable_in A ℳ ≡ ∃φ. φ ↝⇩M ℳ ∧ ℳ ⊨⇘φ⇙ A"

abbreviation is_valid_in ("_ ⊨ _" [50, 50] 50) where
  "ℳ ⊨ A ≡ ∀φ. φ ↝⇩M ℳ ⟶ ℳ ⊨⇘φ⇙ A"

abbreviation is_valid_in_the_general_sense ("⊨ _" [50] 50) where
  "⊨ A ≡ ∀ℳ. is_general_model ℳ ⟶ ℳ ⊨ A"

abbreviation is_valid_in_the_standard_sense ("⊨⇩S _" [50] 50) where
  "⊨⇩S A ≡ ∀ℳ. is_standard_model ℳ ⟶ ℳ ⊨ A"

abbreviation is_true_sentence_in where
  "is_true_sentence_in A ℳ ≡ is_sentence A ∧ ℳ ⊨⇘undefined⇙ A" ― ‹assignments are not meaningful›

abbreviation is_false_sentence_in where
  "is_false_sentence_in A ℳ ≡ is_sentence A ∧ ¬ ℳ ⊨⇘undefined⇙ A" ― ‹assignments are not meaningful›

abbreviation is_model_for where
  "is_model_for ℳ 𝒢 ≡ ∀A ∈ 𝒢. ℳ ⊨ A"

lemma general_validity_in_standard_validity:
  assumes "⊨ A"
  shows "⊨⇩S A"
  using assms and standard_model_is_general_model by blast

end