Theory Consistency

section β€ΉConsistencyβ€Ί

theory Consistency
  imports
    Soundness
begin

definition is_inconsistent_set :: "form set β‡’ bool" where
  [iff]: "is_inconsistent_set 𝒒 ⟷ 𝒒 ⊒ Fo"

definition 𝒬0_is_inconsistent :: bool where
  [iff]: "𝒬0_is_inconsistent ⟷ ⊒ Fo"

definition is_wffo_consistent_with :: "form β‡’ form set β‡’ bool" where
  [iff]: "is_wffo_consistent_with B 𝒒 ⟷ Β¬ is_inconsistent_set (𝒒 βˆͺ {B})"

subsection β€ΉExistence of a standard modelβ€Ί

text β€ΉWe construct a standard model in which β€Ήπ’Ÿ iβ€Ί is the set β€Ή{0}β€Ί:β€Ί

primrec singleton_standard_domain_family ("π’ŸS") where
  "π’ŸS i = 1" ― β€Ήi.e., termβ€Ήπ’ŸS i = set {0}β€Ίβ€Ί
| "π’ŸS o = 𝔹"
| "π’ŸS (Ξ±β†’Ξ²) = π’ŸS Ξ± ⟼ π’ŸS Ξ²"

interpretation singleton_standard_frame: frame "π’ŸS"
proof unfold_locales
  {
    fix Ξ±
    have "π’ŸS Ξ± β‰  0"
    proof (induction Ξ±)
      case (TFun Ξ² Ξ³)
      from β€Ήπ’ŸS Ξ³ β‰  0β€Ί obtain y where "y ∈ elts (π’ŸS Ξ³)"
        by fastforce
      then have "(Ξ»z : π’ŸS Ξ². y) ∈ elts (π’ŸS Ξ² ⟼ π’ŸS Ξ³)"
        by (intro VPi_I)
      then show ?case
        by force
    qed simp_all
  }
  then show "βˆ€Ξ±. π’ŸS Ξ± β‰  0"
    by (intro allI)
qed simp_all

definition singleton_standard_constant_denotation_function ("π’₯S") where
  [simp]: "π’₯S k =
    (
      if
        βˆƒΞ². is_Q_constant_of_type k Ξ²
      then
        let Ξ² = type_of_Q_constant k in qβ‡˜Ξ²β‡™β‡—π’ŸSβ‡–
      else
      if
        is_iota_constant k
      then
        Ξ»z : π’ŸS (iβ†’o). 0
      else
        case k of (c, Ξ±) β‡’ SOME z. z ∈ elts (π’ŸS Ξ±)
    )"

interpretation singleton_standard_premodel: premodel "π’ŸS" "π’₯S"
proof (unfold_locales)
  show "βˆ€Ξ±. π’₯S (Q_constant_of_type Ξ±) = qβ‡˜Ξ±β‡™β‡—π’ŸSβ‡–"
    by simp
next
  show "singleton_standard_frame.is_unique_member_selector (π’₯S iota_constant)"
  unfolding singleton_standard_frame.is_unique_member_selector_def proof
    fix x
    assume "x ∈ elts (π’ŸS i)"
    then have "x = 0"
      by simp
    moreover have "(Ξ»z : π’ŸS (iβ†’o). 0) βˆ™ {0}β‡˜iβ‡™β‡—π’ŸSβ‡– = 0"
      using beta[OF singleton_standard_frame.one_element_function_is_domain_respecting]
      unfolding singleton_standard_domain_family.simps(3) by blast
    ultimately show "(π’₯S iota_constant) βˆ™ {x}β‡˜iβ‡™β‡—π’ŸSβ‡– = x"
      by fastforce
  qed
next
  show "βˆ€c Ξ±. Β¬ is_logical_constant (c, Ξ±) ⟢ π’₯S (c, Ξ±) ∈ elts (π’ŸS Ξ±)"
  proof (intro allI impI)
    fix c and Ξ±
    assume "Β¬ is_logical_constant (c, Ξ±)"
    then have "π’₯S (c, Ξ±) = (SOME z. z ∈ elts (π’ŸS Ξ±))"
      by auto
    moreover have "βˆƒz. z ∈ elts (π’ŸS Ξ±)"
      using eq0_iff and singleton_standard_frame.domain_nonemptiness by presburger
    then have "(SOME z. z ∈ elts (π’ŸS Ξ±)) ∈ elts (π’ŸS Ξ±)"
      using some_in_eq by auto
    ultimately show "π’₯S (c, Ξ±) ∈ elts (π’ŸS Ξ±)"
      by auto
  qed
qed

fun singleton_standard_wff_denotation_function ("𝒱S") where
  "𝒱S Ο† (xβ‡˜Ξ±β‡™) = Ο† (x, Ξ±)"
| "𝒱S Ο† (⦃cβ¦„β‡˜Ξ±β‡™) = π’₯S (c, Ξ±)"
| "𝒱S Ο† (A Β· B) = (𝒱S Ο† A) βˆ™ (𝒱S Ο† B)"
| "𝒱S Ο† (Ξ»xβ‡˜Ξ±β‡™. A) = (Ξ»z : π’ŸS Ξ±. 𝒱S (Ο†((x, Ξ±) := z)) A)"

lemma singleton_standard_wff_denotation_function_closure:
  assumes "frame.is_assignment π’ŸS Ο†"
  and "A ∈ wffsβ‡˜Ξ±β‡™"
  shows "𝒱S Ο† A ∈ elts (π’ŸS Ξ±)"
using assms(2,1) proof (induction A arbitrary: Ο†)
  case (var_is_wff Ξ± x)
  then show ?case
    by simp
next
  case (con_is_wff Ξ± c)
  then show ?case
  proof (cases "(c, Ξ±)" rule: constant_cases)
    case non_logical
    then show ?thesis
      using singleton_standard_premodel.non_logical_constant_denotation
      and singleton_standard_wff_denotation_function.simps(2) by presburger
  next
    case (Q_constant Ξ²)
    then have "𝒱S Ο† (⦃cβ¦„β‡˜Ξ±β‡™) = qβ‡˜Ξ²β‡™β‡—π’ŸSβ‡–"
      by simp
    moreover have "qβ‡˜Ξ²β‡™β‡—π’ŸSβ‡– ∈ elts (π’ŸS (Ξ²β†’Ξ²β†’o))"
      using singleton_standard_domain_family.simps(3)
      and singleton_standard_frame.identity_relation_is_domain_respecting by presburger
    ultimately show ?thesis
      using Q_constant by simp
  next
    case ΞΉ_constant
    then have "𝒱S Ο† (⦃cβ¦„β‡˜Ξ±β‡™) = (Ξ»z : π’ŸS (iβ†’o). 0)"
      by simp
    moreover have "(Ξ»z : π’ŸS (iβ†’o). 0) ∈ elts (π’ŸS ((iβ†’o)β†’i))"
      by (simp add: VPi_I)
    ultimately show ?thesis
      using ΞΉ_constant by simp
  qed
next
  case (app_is_wff Ξ± Ξ² A B)
  have "𝒱S Ο† (A Β· B) = (𝒱S Ο† A) βˆ™ (𝒱S Ο† B)"
    using singleton_standard_wff_denotation_function.simps(3) .
  moreover have "𝒱S Ο† A ∈ elts (π’ŸS (Ξ±β†’Ξ²))" and "𝒱S Ο† B ∈ elts (π’ŸS Ξ±)"
    using app_is_wff.IH and app_is_wff.prems by simp_all
  ultimately show ?case
    by (simp only: singleton_standard_frame.app_is_domain_respecting)
next
  case (abs_is_wff Ξ² A Ξ± x)
  have "𝒱S Ο† (Ξ»xβ‡˜Ξ±β‡™. A) = (Ξ»z : π’ŸS Ξ±. 𝒱S (Ο†((x, Ξ±) := z)) A)"
    using singleton_standard_wff_denotation_function.simps(4) .
  moreover have "𝒱S (Ο†((x, Ξ±) := z)) A ∈ elts (π’ŸS Ξ²)" if "z ∈ elts (π’ŸS Ξ±)" for z
    using that and abs_is_wff.IH and abs_is_wff.prems by simp
  ultimately show ?case
    by (simp add: VPi_I)
qed

interpretation singleton_standard_model: standard_model "π’ŸS" "π’₯S" "𝒱S"
proof (unfold_locales)
  show "singleton_standard_premodel.is_wff_denotation_function 𝒱S"
    by (simp add: singleton_standard_wff_denotation_function_closure)
next
  show "βˆ€Ξ± Ξ². π’ŸS (Ξ±β†’Ξ²) = π’ŸS Ξ± ⟼ π’ŸS Ξ²"
    using singleton_standard_domain_family.simps(3) by (intro allI)
qed

proposition standard_model_existence:
  shows "βˆƒβ„³. is_standard_model β„³"
  using singleton_standard_model.standard_model_axioms by auto

subsection β€ΉTheorem 5403 (Consistency Theorem)β€Ί

proposition model_existence_implies_set_consistency:
  assumes "is_hyps 𝒒"
  and "βˆƒβ„³. is_general_model β„³ ∧ is_model_for β„³ 𝒒"
  shows "Β¬ is_inconsistent_set 𝒒"
proof (rule ccontr)
  from assms(2) obtain π’Ÿ and π’₯ and 𝒱 and β„³
    where "β„³ = (π’Ÿ, π’₯, 𝒱)" and "is_model_for β„³ 𝒒" and "is_general_model β„³" by fastforce
  assume "Β¬ Β¬ is_inconsistent_set 𝒒"
  then have "𝒒 ⊒ Fo"
    by simp
  with β€Ήis_general_model β„³β€Ί have "β„³ ⊨ Fo"
    using thm_5402(2)[OF assms(1) β€Ήis_model_for β„³ 𝒒›] by simp
  then have "𝒱 Ο† Fo = T" if "Ο† ↝ π’Ÿ" for Ο†
    using that and β€Ήβ„³ = (π’Ÿ, π’₯, 𝒱)β€Ί by force
  moreover have "𝒱 Ο† Fo = F" if "Ο† ↝ π’Ÿ" for Ο†
    using β€Ήβ„³ = (π’Ÿ, π’₯, 𝒱)β€Ί and β€Ήis_general_model β„³β€Ί and that and general_model.prop_5401_d
    by simp
  ultimately have "βˆ„Ο†. Ο† ↝ π’Ÿ"
    by (auto simp add: inj_eq)
  moreover have "βˆƒΟ†. Ο† ↝ π’Ÿ"
  proof -
    ― β€Ή
      Since by definition domains are not empty then, by using the Axiom of Choice, we can specify
      an assignment β€ΉΟˆβ€Ί that simply chooses some element in the respective domain for each variable.
      Nonetheless, as pointed out in Footnote 11, page 19 in citeβ€Ή"andrews:1965"β€Ί, it is not
      necessary to use the Axiom of Choice to show that assignments exist since some assignments
      can be described explicitly.
    β€Ί
    let ?ψ = "Ξ»v. case v of (_, Ξ±) β‡’ SOME z. z ∈ elts (π’Ÿ Ξ±)"
    from β€Ήβ„³ = (π’Ÿ, π’₯, 𝒱)β€Ί and β€Ήis_general_model β„³β€Ί have "βˆ€Ξ±. elts (π’Ÿ Ξ±) β‰  {}"
      using frame.domain_nonemptiness and premodel_def and general_model.axioms(1) by auto
    with β€Ήβ„³ = (π’Ÿ, π’₯, 𝒱)β€Ί and β€Ήis_general_model β„³β€Ί have "?ψ ↝ π’Ÿ"
      using frame.is_assignment_def and premodel_def and general_model.axioms(1)
      by (metis (mono_tags) case_prod_conv some_in_eq)
    then show ?thesis
      by (intro exI)
  qed
  ultimately show False ..
qed

proposition 𝒬0_is_consistent:
  shows "Β¬ 𝒬0_is_inconsistent"
proof -
  have "βˆƒβ„³. is_general_model β„³ ∧ is_model_for β„³ {}"
    using standard_model_existence and standard_model.axioms(1) by blast
  then show ?thesis
    using model_existence_implies_set_consistency by simp
qed

lemmas thm_5403 = 𝒬0_is_consistent model_existence_implies_set_consistency

proposition principle_of_explosion:
  assumes "is_hyps 𝒒"
  shows "is_inconsistent_set 𝒒 ⟷ (βˆ€A ∈ (wffsβ‡˜o⇙). 𝒒 ⊒ A)"
proof
  assume "is_inconsistent_set 𝒒"
  show "βˆ€A ∈ (wffsβ‡˜o⇙). 𝒒 ⊒ A"
  proof
    fix A
    assume "A ∈ wffsβ‡˜o⇙"
    from β€Ήis_inconsistent_set 𝒒› have "𝒒 ⊒ Fo"
      unfolding is_inconsistent_set_def .
    then have "𝒒 ⊒ βˆ€π”΅β‡˜o⇙. π”΅β‡˜o⇙"
      unfolding false_is_forall .
    with β€ΉA ∈ wffsβ‡˜o⇙› have "𝒒 ⊒ S {(𝔡, o) ↣ A} (π”΅β‡˜o⇙)"
      using "βˆ€I" by fastforce
    then show "𝒒 ⊒ A"
      by simp
  qed
next
  assume "βˆ€A ∈ (wffsβ‡˜o⇙). 𝒒 ⊒ A"
  then have "𝒒 ⊒ Fo"
    using false_wff by (elim bspec)
  then show "is_inconsistent_set 𝒒"
    unfolding is_inconsistent_set_def .
qed

end