# 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
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. δ φ ≤ (∑ψ←Ψ. δ ψ))"
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
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 Ψ. δ ψ))"
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
next
case (Cons φ Φ)
assume "⊢ ∐ (φ # Φ)"
hence "⊢ ∼ (φ ⊓ ⨆ Φ)" "⊢ ∐ Φ" by simp+
hence "𝒫 (⨆(φ # Φ)) = 𝒫 φ + 𝒫 (⨆ Φ)"
"𝒫 (⨆ Φ) = (∑φ←Φ. 𝒫 φ)"
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 moura
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 "⊢ ∐ [φ]"
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 "⊢ ∐ [φ]"
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 "(∑φ←Φ. 𝒫 φ) = 𝒫 (⨆ Φ)"