Theory Suppes_Theorem

chapter ‹ Suppes' Theorem \label{sec:suppes-theorem} ›

theory Suppes_Theorem
  imports Probability_Logic
begin

no_notation FuncSet.funcset (infixr "→" 60)

text ‹ An elementary completeness theorem for inequalities for probability logic
       is due to Patrick Suppes @{cite suppesProbabilisticInferenceConcept1966}. ›

text ‹ A consequence of this Suppes' theorem is an elementary form of ∗‹collapse›,
       which asserts that inequalities for probabilities are logically
       equivalent to the more restricted class of ∗‹Dirac measures› as
       defined in \S\ref{sec:dirac-measures}. ›

section ‹ Suppes' List Theorem \label{sec:suppes-theorem-for-lists} ›

text ‹ We first establish Suppes' theorem for lists of propositions. This
       is done by establishing our first completeness theorem using
       ∗‹Dirac measures›. ›

text ‹ First, we use the result from \S\ref{sec:basic-probability-inequality-results}
       that shows ‹⊢ φ → ⨆ Ψ› implies ‹𝒫 φ ≤ (∑ψ←Ψ. 𝒫 ψ)›.
       This can be understood as a ∗‹soundness› result. ›

text ‹ To show completeness, assume ‹¬ ⊢ φ → ⨆ Ψ›. From this
       obtain a maximally consistent \<^term>‹Ω› such that ‹φ → ⨆ Ψ ∉ Ω›. 
       We then define \<^term>‹δ χ = (if (χ ∈ Ω) then 1 else 0)› and 
       show \<^term>‹δ› is a  ∗‹Dirac measure› such that ‹δ φ ≤ (∑ψ←Ψ. δ ψ)›. ›

lemma (in classical_logic) dirac_list_summation_completeness:
  "(∀ δ ∈ dirac_measures. δ φ ≤ (∑ψ←Ψ. δ ψ)) = ⊢ φ → ⨆ Ψ"
proof -
  {
    fix δ :: "'a ⇒ real"
    assume "δ ∈ dirac_measures"
    from this interpret probability_logic "(λ φ. ⊢ φ)" "(→)" "⊥" "δ"
      unfolding dirac_measures_def
      by auto
    assume "⊢ φ → ⨆ Ψ"
    hence "δ φ ≤ (∑ψ←Ψ. δ ψ)"
      using implication_list_summation_inequality
      by auto
  }
  moreover {
    assume "¬ ⊢ φ → ⨆ Ψ"
    from this obtain Ω where Ω:
      "MCS Ω"
      "φ ∈ Ω"
      "⨆ Ψ ∉ Ω"
      by (meson
            insert_subset
            formula_consistent_def
            formula_maximal_consistency
            formula_maximally_consistent_extension
            formula_maximally_consistent_set_def_def
            set_deduction_base_theory
            set_deduction_reflection
            set_deduction_theorem)
    hence"∀ ψ ∈ set Ψ. ψ ∉ Ω"
      using arbitrary_disjunction_exclusion_MCS by blast
    define δ where "δ = (λ χ . if χ∈Ω then (1 :: real) else 0)"
    from ‹∀ ψ ∈ set Ψ. ψ ∉ Ω› have "(∑ψ←Ψ. δ ψ) = 0"
      unfolding δ_def
      by (induct Ψ, simp, simp)
    hence "¬ δ φ ≤ (∑ψ←Ψ. δ ψ)"
      unfolding δ_def
      by (simp add: Ω(2))
    hence
      "∃ δ ∈ dirac_measures. ¬ (δ φ ≤ (∑ψ←Ψ. δ ψ))"
      unfolding δ_def
      using Ω(1) MCS_dirac_measure by auto
  }
  ultimately show ?thesis by blast
qed

theorem (in classical_logic) list_summation_completeness:
  "(∀ 𝒫 ∈ probabilities. 𝒫 φ ≤ (∑ψ←Ψ. 𝒫 ψ)) = ⊢ φ → ⨆ Ψ"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  hence "∀ δ ∈ dirac_measures. δ φ ≤ (∑ψ←Ψ. δ ψ)"
    unfolding dirac_measures_def probabilities_def
    by blast
  thus ?rhs
    using dirac_list_summation_completeness by blast
next
  assume ?rhs
  show ?lhs
  proof
    fix 𝒫 :: "'a ⇒ real"
    assume "𝒫 ∈ probabilities"
    from this interpret probability_logic "(λ φ. ⊢ φ)" "(→)" ⊥ 𝒫
      unfolding probabilities_def
      by auto
    show "𝒫 φ ≤ (∑ψ←Ψ. 𝒫 ψ)"
      using ‹?rhs› implication_list_summation_inequality
      by simp
  qed
qed

text ‹ The collapse theorem asserts that to prove an inequalities for all 
       probabilities in probability logic, one only needs to consider the 
       case of functions which take on values of 0 or 1. ›

lemma (in classical_logic) suppes_collapse:
  "(∀ 𝒫 ∈ probabilities. 𝒫 φ ≤ (∑ψ←Ψ. 𝒫 ψ))
      = (∀ δ ∈ dirac_measures. δ φ ≤ (∑ψ←Ψ. δ ψ))"
  by (simp add:
        dirac_list_summation_completeness
        list_summation_completeness)

lemma (in classical_logic) probability_member_neg:
  fixes 𝒫
  assumes "𝒫 ∈ probabilities"
  shows "𝒫 (∼ φ) = 1 - 𝒫 φ"
proof -
  from assms interpret probability_logic "(λ φ. ⊢ φ)" "(→)" ⊥ 𝒫
    unfolding probabilities_def
    by auto
  show ?thesis
    by (simp add: complementation)
qed

text ‹ Suppes' theorem has a philosophical interpretation.
       It asserts that if \<^term>‹Ψ :⊢ φ›, then our ∗‹uncertainty›
       in \<^term>‹φ› is bounded above by our uncertainty in \<^term>‹Ψ›.
       Here the uncertainty in the proposition \<^term>‹φ› is ‹1 - 𝒫 φ›.
       Our uncertainty in \<^term>‹Ψ›, on the other hand, is
       ‹∑ψ←Ψ. 1 - 𝒫 ψ›. ›

theorem (in classical_logic) suppes_list_theorem:
  "Ψ :⊢ φ = (∀ 𝒫 ∈ probabilities. (∑ψ←Ψ. 1 - 𝒫 ψ) ≥ 1 - 𝒫 φ)"
proof -
  have
    "Ψ :⊢ φ = (∀ 𝒫 ∈ probabilities. (∑ψ ← ❙∼ Ψ. 𝒫 ψ) ≥ 𝒫 (∼ φ))"
    using
      list_summation_completeness
      weak_biconditional_weaken
      contra_list_curry_uncurry
      list_deduction_def
    by blast
  moreover have
    "∀ 𝒫 ∈ probabilities. (∑ψ ← (❙∼ Ψ). 𝒫 ψ) = (∑ψ ← Ψ. 𝒫 (∼ ψ))"
    by (induct Ψ, auto)
  ultimately show ?thesis
    using probability_member_neg
    by (induct Ψ, simp+)
qed

section ‹ Suppes' Set Theorem ›

text ‹ Suppes theorem also obtains for ∗‹sets›. ›

lemma (in classical_logic) dirac_set_summation_completeness:
  "(∀ δ ∈ dirac_measures. δ φ ≤ (∑ψ∈ set Ψ. δ ψ)) = ⊢ φ → ⨆ Ψ"
  by (metis
        dirac_list_summation_completeness
        modus_ponens
        arbitrary_disjunction_remdups
        biconditional_left_elimination
        biconditional_right_elimination
        hypothetical_syllogism
        sum.set_conv_list)

theorem (in classical_logic) set_summation_completeness:
  "(∀ δ ∈ probabilities. δ φ ≤ (∑ψ∈ set Ψ. δ ψ)) = ⊢ φ → ⨆ Ψ"
  by (metis
        dirac_list_summation_completeness
        dirac_set_summation_completeness
        list_summation_completeness
        sum.set_conv_list)

lemma (in classical_logic) suppes_set_collapse:
  "(∀ 𝒫 ∈ probabilities. 𝒫 φ ≤ (∑ψ ∈ set Ψ. 𝒫 ψ))
      = (∀ δ ∈ dirac_measures. δ φ ≤ (∑ψ ∈ set Ψ. δ ψ))"
  by (simp add:
        dirac_set_summation_completeness
        set_summation_completeness)

text ‹ In our formulation of logic, there is not reason that ‹∼ a = ∼ b›
       while \<^term>‹a ≠ b›.  As a consequence the Suppes theorem
       for sets presented below is different than the one given in
       \S\ref{sec:suppes-theorem-for-lists}. ›

theorem (in classical_logic) suppes_set_theorem:
  "Ψ :⊢ φ
     = (∀ 𝒫 ∈ probabilities. (∑ψ ∈ set (❙∼ Ψ). 𝒫 ψ) ≥ 1 - 𝒫 φ)"
proof -
  have "Ψ :⊢ φ
          = (∀ 𝒫 ∈ probabilities. (∑ψ ∈ set (❙∼ Ψ). 𝒫 ψ) ≥ 𝒫 (∼ φ))"
    using
      contra_list_curry_uncurry
      list_deduction_def
      set_summation_completeness
      weak_biconditional_weaken
    by blast
  thus ?thesis
    using probability_member_neg
    by (induct Ψ, auto)
qed

section ‹ Converse Suppes' Theorem ›

text ‹ A formulation of the converse of Suppes' theorem obtains
       for lists/sets of ∗‹logically disjoint› propositions. ›

lemma (in probability_logic) exclusive_sum_list_identity:
  assumes "⊢ ∐ Φ"
  shows "𝒫 (⨆ Φ) = (∑φ←Φ. 𝒫 φ)"
  using assms
proof (induct Φ)
  case Nil
  then show ?case
    by (simp add: gaines_weatherson_antithesis)
next
  case (Cons φ Φ)
  assume "⊢ ∐ (φ # Φ)"
  hence "⊢ ∼ (φ ⊓ ⨆ Φ)" "⊢ ∐ Φ" by simp+
  hence "𝒫 (⨆(φ # Φ)) = 𝒫 φ + 𝒫 (⨆ Φ)"
        "𝒫 (⨆ Φ) = (∑φ←Φ. 𝒫 φ)"
    using Cons.hyps probability_additivity by auto
  hence "𝒫 (⨆(φ # Φ)) = 𝒫 φ + (∑φ←Φ. 𝒫 φ)" by auto
  thus ?case by simp
qed

lemma sum_list_monotone:
  fixes f :: "'a ⇒ real"
  assumes "∀ x. f x ≥ 0"
     and  "set Φ ⊆ set Ψ"
     and  "distinct Φ"
   shows "(∑φ←Φ. f φ) ≤ (∑ψ←Ψ. f ψ)"
  using assms
proof -
  assume "∀ x. f x ≥ 0"
  have "∀Φ. set Φ ⊆ set Ψ
             ⟶ distinct Φ
             ⟶ (∑φ←Φ. f φ) ≤ (∑ψ←Ψ. f ψ)"
  proof (induct Ψ)
    case Nil
    then show ?case by simp
  next
    case (Cons ψ Ψ)
    {
      fix Φ
      assume "set Φ ⊆ set (ψ # Ψ)"
         and "distinct Φ"
      have "(∑φ←Φ. f φ) ≤ (∑ψ'←(ψ # Ψ). f ψ')"
      proof -
        {
          assume "ψ ∉ set Φ"
          with ‹set Φ ⊆ set (ψ # Ψ)› have "set Φ ⊆ set Ψ" by auto
          hence "(∑φ←Φ. f φ) ≤ (∑ψ←Ψ. f ψ)"
            using Cons.hyps ‹distinct Φ› by auto
          moreover have "f ψ ≥ 0" using ‹∀ x. f x ≥ 0› by metis
          ultimately have ?thesis by simp
        }
        moreover
        {
          assume "ψ ∈ set Φ"
          hence "set Φ = insert ψ (set (removeAll ψ Φ))"
            by auto
          with ‹set Φ ⊆ set (ψ # Ψ)› have "set (removeAll ψ Φ) ⊆ set Ψ"
            by (metis
                  insert_subset
                  list.simps(15)
                  set_removeAll
                  subset_insert_iff)
          moreover from ‹distinct Φ› have "distinct (removeAll ψ Φ)"
            by (meson distinct_removeAll)
          ultimately have "(∑φ←(removeAll ψ Φ). f φ) ≤ (∑ψ←Ψ. f ψ)"
            using Cons.hyps
            by simp
          moreover from ‹ψ ∈ set Φ› ‹distinct Φ›
          have "(∑φ←Φ. f φ) = f ψ + (∑φ←(removeAll ψ Φ). f φ)"
            using distinct_remove1_removeAll sum_list_map_remove1
            by fastforce
          ultimately have ?thesis using ‹∀ x. f x ≥ 0›
            by simp
        }
        ultimately show ?thesis by blast
      qed
    }
    thus ?case by blast
  qed
  moreover assume "set Φ ⊆ set Ψ" and "distinct Φ"
  ultimately show ?thesis by blast
qed

lemma count_remove_all_sum_list:
  fixes f :: "'a ⇒ real"
  shows "real (count_list xs x) * f x + (∑x'←(removeAll x xs). f x')
           = (∑x←xs. f x)"
  by (induct xs, simp, simp, metis combine_common_factor mult_cancel_right1)

lemma (in classical_logic) dirac_exclusive_implication_completeness:
  "(∀ δ ∈ dirac_measures. (∑φ←Φ. δ φ) ≤ δ ψ) = (⊢ ∐ Φ ∧  ⊢ ⨆ Φ → ψ)"
proof -
  {
    fix δ
    assume "δ ∈ dirac_measures"
    from this interpret probability_logic "(λ φ. ⊢ φ)" "(→)" "⊥" "δ"
      unfolding dirac_measures_def
      by simp
    assume "⊢ ∐ Φ" "⊢ ⨆ Φ → ψ"
    hence "(∑φ←Φ. δ φ) ≤ δ ψ"
      using exclusive_sum_list_identity monotonicity by fastforce
  }
  moreover
  {
    assume "¬ ⊢ ∐ Φ"
    hence "(∃ φ ∈ set Φ. ∃ ψ ∈ set Φ.
              φ ≠ ψ ∧ ¬ ⊢ ∼ (φ ⊓ ψ)) ∨ (∃ φ ∈ duplicates Φ. ¬ ⊢ ∼ φ)"
      using exclusive_equivalence set_deduction_base_theory by blast
    hence "¬ (∀ δ ∈ dirac_measures. (∑φ←Φ. δ φ) ≤ δ ψ)"
    proof (elim disjE)
      assume "∃ φ ∈ set Φ. ∃ χ ∈ set Φ. φ ≠ χ ∧ ¬ ⊢ ∼ (φ ⊓ χ)"
      from this obtain φ and χ
        where φχ_properties:
          "φ ∈ set Φ"
          "χ ∈ set Φ"
          "φ ≠ χ"
          "¬ ⊢ ∼ (φ ⊓ χ)"
        by blast
      from this obtain Ω where Ω: "MCS Ω" "∼ (φ ⊓ χ) ∉ Ω"
        by (meson
              insert_subset
              formula_consistent_def
              formula_maximal_consistency
              formula_maximally_consistent_extension
              formula_maximally_consistent_set_def_def
              set_deduction_base_theory
              set_deduction_reflection
              set_deduction_theorem)
      let ?δ = "λ χ. if χ∈Ω then (1 :: real) else 0"
      from Ω have "φ ∈ Ω" "χ ∈ Ω"
        by (metis
              formula_maximally_consistent_set_def_implication
              maximally_consistent_set_def
              conjunction_def
              negation_def)+
      with φχ_properties have
          "(∑φ←[φ, χ]. ?δ φ) = 2"
          "set [φ, χ] ⊆ set Φ"
          "distinct [φ, χ]"
          "∀φ. ?δ φ ≥ 0"
        by simp+
      hence "(∑φ←Φ. ?δ φ) ≥ 2" using sum_list_monotone by metis
      hence "¬ (∑φ←Φ. ?δ φ) ≤ ?δ (ψ)" by auto
      thus ?thesis
        using Ω(1) MCS_dirac_measure
        by auto
    next
      assume "∃ φ ∈ duplicates Φ. ¬ ⊢ ∼ φ"
      from this obtain φ where φ: "φ ∈ duplicates Φ" "¬ ⊢ ∼ φ"
        using
          exclusive_equivalence [where Γ="{}"]
          set_deduction_base_theory
        by blast
      from φ obtain Ω where Ω: "MCS Ω" "∼ φ ∉ Ω"
        by (meson
              insert_subset
              formula_consistent_def
              formula_maximal_consistency
              formula_maximally_consistent_extension
              formula_maximally_consistent_set_def_def
              set_deduction_base_theory
              set_deduction_reflection
              set_deduction_theorem)
      hence "φ ∈ Ω"
        using negation_def by auto
      let ?δ = "λ χ. if χ∈Ω then (1 :: real) else 0"
      from φ have "count_list Φ φ ≥ 2"
        using duplicates_alt_def [where xs="Φ"]
        by blast
      hence "real (count_list Φ φ) * ?δ φ ≥ 2" using ‹φ ∈ Ω› by simp
      moreover
      {
        fix Ψ
        have "(∑φ←Ψ. ?δ φ) ≥ 0" by (induct Ψ, simp, simp)
      }
      moreover have "(0::real)
                          ≤ (∑a←removeAll φ Φ. if a ∈ Ω then 1 else 0)"
        using ‹⋀Ψ. 0 ≤ (∑φ←Ψ. if φ ∈ Ω then 1 else 0)›
        by presburger
      ultimately have "real (count_list Φ φ) * ?δ φ
                            + (∑ φ ← (removeAll φ Φ). ?δ φ) ≥ 2"
        using ‹2 ≤ real (count_list Φ φ) * (if φ ∈ Ω then 1 else 0)›
        by linarith
      hence "(∑φ←Φ. ?δ φ) ≥ 2" by (metis count_remove_all_sum_list)
      hence "¬ (∑φ←Φ. ?δ φ) ≤ ?δ (ψ)" by auto
      thus ?thesis
        using Ω(1) MCS_dirac_measure
        by auto
    qed
  }
  moreover
  {
    assume "¬ ⊢ ⨆ Φ → ψ"
    from this obtain Ω φ
      where
        Ω: "MCS Ω"
        and ψ: "ψ ∉ Ω"
        and φ: "φ ∈ set Φ" "φ ∈ Ω"
      by (meson
            insert_subset
            formula_consistent_def
            formula_maximal_consistency
            formula_maximally_consistent_extension
            formula_maximally_consistent_set_def_def
            arbitrary_disjunction_exclusion_MCS
            set_deduction_base_theory
            set_deduction_reflection
            set_deduction_theorem)
    let ?δ = "λ χ. if χ∈Ω then (1 :: real) else 0"
    from φ have "(∑φ←Φ. ?δ φ) ≥ 1"
    proof (induct Φ)
      case Nil
      then show ?case by simp
    next
      case (Cons φ' Φ)
      obtain f :: "real list ⇒ real" where f:
        "∀rs. f rs ∈ set rs ∧ ¬ 0 ≤ f rs ∨ 0 ≤ sum_list rs"
        using sum_list_nonneg by metis
      moreover have "f (map ?δ Φ) ∉ set (map ?δ Φ) ∨ 0 ≤ f (map ?δ Φ)"
        by fastforce
      ultimately show ?case
        by (simp, metis Cons.hyps Cons.prems(1) φ(2) set_ConsD)
    qed
    hence "¬ (∑φ←Φ. ?δ φ) ≤ ?δ (ψ)" using ψ by auto
    hence "¬ (∀ δ ∈ dirac_measures. (∑φ←Φ. δ φ) ≤ δ ψ)"
      using Ω(1) MCS_dirac_measure
      by auto
  }
  ultimately show ?thesis by blast
qed

theorem (in classical_logic) exclusive_implication_completeness:
  "(∀ 𝒫 ∈ probabilities. (∑φ←Φ. 𝒫 φ) ≤ 𝒫 ψ) = (⊢ ∐ Φ ∧  ⊢ ⨆ Φ → ψ)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  thus ?rhs
    by (meson
          dirac_exclusive_implication_completeness
          dirac_measures_subset
          subset_eq)
next
  assume ?rhs
  show ?lhs
  proof
    fix 𝒫 :: "'a ⇒ real"
    assume "𝒫 ∈ probabilities"
    from this interpret probability_logic "(λ φ. ⊢ φ)" "(→)" ⊥ 𝒫
      unfolding probabilities_def
      by simp
    show "(∑φ←Φ. 𝒫 φ) ≤ 𝒫 ψ"
      using
        ‹?rhs›
        exclusive_sum_list_identity
        monotonicity
      by fastforce
  qed
qed

lemma (in classical_logic) dirac_inequality_completeness:
  "(∀ δ ∈ dirac_measures. δ φ ≤ δ ψ) = ⊢ φ → ψ"
proof -
  have "⊢ ∐ [φ]"
    by (simp add: conjunction_right_elimination negation_def)
  hence "(⊢ ∐ [φ] ∧  ⊢ ⨆ [φ] → ψ) = ⊢ φ → ψ"
    by (metis
          arbitrary_disjunction.simps(1)
          arbitrary_disjunction.simps(2)
          disjunction_def implication_equivalence
          negation_def
          weak_biconditional_weaken)
  thus ?thesis
    using dirac_exclusive_implication_completeness [where Φ="[φ]"]
    by auto
qed

section ‹ Implication Inequality Completeness ›

text ‹ The following theorem establishes the converse of
       ‹⊢ φ → ψ ⟹ 𝒫 φ ≤ 𝒫 ψ›, which was
       proved in \S\ref{sec:prob-logic-alt-def}. ›

theorem (in classical_logic) implication_inequality_completeness:
  "(∀ 𝒫 ∈ probabilities. 𝒫 φ ≤ 𝒫 ψ) = ⊢ φ → ψ"
proof -
  have "⊢ ∐ [φ]"
    by (simp add: conjunction_right_elimination negation_def)
  hence "(⊢ ∐ [φ] ∧  ⊢ ⨆ [φ] → ψ) = ⊢ φ → ψ"
    by (metis
          arbitrary_disjunction.simps(1)
          arbitrary_disjunction.simps(2)
          disjunction_def implication_equivalence
          negation_def
          weak_biconditional_weaken)
  thus ?thesis
    using exclusive_implication_completeness [where Φ="[φ]"]
    by simp
qed

section ‹ Characterizing Logical Exclusiveness In Probability Logic ›

text ‹ Finally, we can say that ‹𝒫 (⨆ Φ) = (∑φ←Φ. 𝒫 φ)› if and only
       if the propositions in \<^term>‹Φ› are mutually exclusive (i.e. ‹⊢ ∐ Φ›).
       This result also obtains for sets. ›

lemma (in classical_logic) dirac_exclusive_list_summation_completeness:
  "(∀ δ ∈ dirac_measures. δ (⨆ Φ) = (∑φ←Φ. δ φ)) = ⊢ ∐ Φ"
  by (metis
        antisym_conv
        dirac_exclusive_implication_completeness
        dirac_list_summation_completeness
        trivial_implication)

theorem (in classical_logic) exclusive_list_summation_completeness:
  "(∀ 𝒫 ∈ probabilities. 𝒫 (⨆ Φ) = (∑φ←Φ. 𝒫 φ)) = ⊢ ∐ Φ"
  by (metis
        antisym_conv
        exclusive_implication_completeness
        list_summation_completeness
        trivial_implication)

lemma (in classical_logic) dirac_exclusive_set_summation_completeness:
  "(∀ δ ∈ dirac_measures. δ (⨆ Φ) = (∑φ ∈ set Φ. δ φ))
      = ⊢ ∐ (remdups Φ)"
  by (metis
        (mono_tags)
        eq_iff
        dirac_exclusive_implication_completeness
        dirac_set_summation_completeness
        trivial_implication
        set_remdups
        sum.set_conv_list    eq_iff
        dirac_exclusive_implication_completeness
        dirac_set_summation_completeness
        trivial_implication
        set_remdups
        sum.set_conv_list
        antisym_conv)

theorem (in classical_logic) exclusive_set_summation_completeness:
  "(∀ 𝒫 ∈ probabilities.
        𝒫 (⨆ Φ) = (∑φ ∈ set Φ. 𝒫 φ)) = ⊢ ∐ (remdups Φ)"
  by (metis
        (mono_tags, opaque_lifting)
        antisym_conv
        exclusive_list_summation_completeness
        exclusive_implication_completeness
        implication_inequality_completeness
        set_summation_completeness
        order.refl
        sum.set_conv_list)

lemma (in probability_logic) exclusive_list_set_inequality:
  assumes "⊢ ∐ Φ"
  shows "(∑φ←Φ. 𝒫 φ) = (∑φ∈set Φ. 𝒫 φ)"
proof -
  have "distinct (remdups Φ)" using distinct_remdups by auto
  hence "duplicates (remdups Φ) = {}"
    by (induct "Φ", simp+)
  moreover have "set (remdups Φ) = set Φ"
    by (induct "Φ", simp, simp add: insert_absorb)
  moreover have "(∀φ ∈ duplicates Φ. ⊢ ∼ φ)
               ∧ (∀ φ ∈ set Φ. ∀ ψ ∈ set Φ. (φ ≠ ψ) ⟶ ⊢ ∼ (φ ⊓ ψ))"
    using
      assms
      exclusive_elimination1
      exclusive_elimination2
      set_deduction_base_theory
    by blast
  ultimately have
    "(∀φ∈duplicates (remdups Φ). ⊢ ∼ φ)
   ∧ (∀ φ ∈ set (remdups Φ). ∀ ψ ∈ set (remdups Φ).
          (φ ≠ ψ) ⟶ ⊢ ∼ (φ ⊓ ψ))"
    by auto
  hence "⊢ ∐ (remdups Φ)"
    by (meson exclusive_equivalence set_deduction_base_theory)
  hence "(∑φ∈set Φ. 𝒫 φ) = 𝒫 (⨆ Φ)"
    by (metis
          arbitrary_disjunction_remdups
          biconditional_equivalence
          exclusive_sum_list_identity
          sum.set_conv_list)
  moreover have "(∑φ←Φ. 𝒫 φ) = 𝒫 (⨆ Φ)"
    by (simp add: assms exclusive_sum_list_identity)
  ultimately show ?thesis by metis
qed

notation FuncSet.funcset (infixr "→" 60)

end