Theory GEM
section ‹ General Extensional Mereology ›
theory GEM
imports GMM CEM
begin
text ‹ The theory of \emph{general extensional mereology}, also known as \emph{classical extensional
mereology} adds general mereology to extensional mereology.\footnote{For this axiomatization see
\<^cite>‹"varzi_parts_1996"› p. 265 and \<^cite>‹"casati_parts_1999"› p. 46.} ›
locale GEM = GM + EM +
assumes sum_eq: "x ⊕ y = (THE z. ∀v. O v z ⟷ O v x ∨ O v y)"
assumes product_eq:
"x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)"
assumes difference_eq:
"x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))"
assumes complement_eq: "─ x = (THE z. ∀w. P w z ⟷ ¬ O w x)"
assumes universe_eq: "u = (THE x. ∀y. P y x)"
assumes fusion_eq: "∃x. F x ⟹
(σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))"
assumes general_product_eq: "(π x. F x) = (σ x. ∀y. F y ⟶ P x y)"
sublocale GEM ⊆ GMM
proof
qed
subsection ‹ General Sums ›
context GEM
begin
lemma fusion_intro:
"(∀y. O y z ⟷ (∃x. F x ∧ O y x)) ⟹ (σ x. F x) = z"
proof -
assume antecedent: "(∀y. O y z ⟷ (∃x. F x ∧ O y x))"
hence "(THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z)) = z"
proof (rule the_equality)
fix a
assume a: "(∀y. O y a ⟷ (∃x. F x ∧ O y x))"
have "∀x. O x a ⟷ O x z"
proof
fix b
from antecedent have "O b z ⟷ (∃x. F x ∧ O b x)"..
moreover from a have "O b a ⟷ (∃x. F x ∧ O b x)"..
ultimately show "O b a ⟷ O b z" by (rule ssubst)
qed
with overlap_extensionality show "a = z"..
qed
moreover from antecedent have "O z z ⟷ (∃x. F x ∧ O z x)"..
hence "∃x. F x ∧ O z x" using overlap_reflexivity..
hence "∃x. F x" by auto
hence "(σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))"
by (rule fusion_eq)
ultimately show "(σ v. F v) = z" by (rule subst)
qed
lemma fusion_idempotence: "(σ x. z = x) = z"
proof -
have "∀y. O y z ⟷ (∃x. z = x ∧ O y x)"
proof
fix y
show "O y z ⟷ (∃x. z = x ∧ O y x)"
proof
assume "O y z"
with refl have "z = z ∧ O y z"..
thus "∃x. z = x ∧ O y x"..
next
assume "∃x. z = x ∧ O y x"
then obtain x where x: "z = x ∧ O y x"..
hence "z = x"..
moreover from x have "O y x"..
ultimately show "O y z" by (rule ssubst)
qed
qed
thus "(σ x. z = x) = z"
by (rule fusion_intro)
qed
text ‹ The whole is the sum of its parts. ›
lemma fusion_absorption: "(σ x. P x z) = z"
proof -
have "(∀y. O y z ⟷ (∃x. P x z ∧ O y x))"
proof
fix y
show "O y z ⟷ (∃x. P x z ∧ O y x)"
proof
assume "O y z"
with part_reflexivity have "P z z ∧ O y z"..
thus "∃x. P x z ∧ O y x"..
next
assume "∃x. P x z ∧ O y x"
then obtain x where x: "P x z ∧ O y x"..
hence "P x z"..
moreover from x have "O y x"..
ultimately show "O y z" by (rule overlap_monotonicity)
qed
qed
thus "(σ x. P x z) = z"
by (rule fusion_intro)
qed
lemma part_fusion: "P w (σ v. P v x) ⟹ P w x"
proof -
assume "P w (σ v. P v x)"
with fusion_absorption show "P w x" by (rule subst)
qed
lemma fusion_character:
"∃x. F x ⟹ (∀y. O y (σ v. F v) ⟷ (∃x. F x ∧ O y x))"
proof -
assume "∃x. F x"
hence "∃z. ∀y. O y z ⟷ (∃x. F x ∧ O y x)"
by (rule fusion)
then obtain z where z: "∀y. O y z ⟷ (∃x. F x ∧ O y x)"..
hence "(σ v. F v) = z " by (rule fusion_intro)
thus "∀y. O y (σ v. F v) ⟷ (∃x. F x ∧ O y x)" using z by (rule ssubst)
qed
text ‹ The next lemma characterises fusions in terms of parthood.\footnote{See \<^cite>‹"pontow_note_2004"› pp. 202-9.} ›
lemma fusion_part_character: "∃x. F x ⟹
(∀y. P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v)))"
proof -
assume "(∃x. F x)"
hence F: "∀y. O y (σ v. F v) ⟷ (∃x. F x ∧ O y x)"
by (rule fusion_character)
show "∀y. P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"
proof
fix y
show "P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"
proof
assume "P y (σ v. F v)"
show "∀w. P w y ⟶ (∃v. F v ∧ O w v)"
proof
fix w
from F have w: "O w (σ v. F v) ⟷ (∃x. F x ∧ O w x)"..
show "P w y ⟶ (∃v. F v ∧ O w v)"
proof
assume "P w y"
hence "P w (σ v. F v)" using ‹P y (σ v. F v)›
by (rule part_transitivity)
hence "O w (σ v. F v)" by (rule part_implies_overlap)
with w show "∃x. F x ∧ O w x"..
qed
qed
next
assume right: "∀w. P w y ⟶ (∃v. F v ∧ O w v)"
show "P y (σ v. F v)"
proof (rule ccontr)
assume "¬ P y (σ v. F v)"
hence "∃v. P v y ∧ ¬ O v (σ v. F v)"
by (rule strong_supplementation)
then obtain v where v: "P v y ∧ ¬ O v (σ v. F v)"..
hence "¬ O v (σ v. F v)"..
from right have "P v y ⟶ (∃w. F w ∧ O v w)"..
moreover from v have "P v y"..
ultimately have "∃w. F w ∧ O v w"..
from F have "O v (σ v. F v) ⟷ (∃x. F x ∧ O v x)"..
hence "O v (σ v. F v)" using ‹∃w. F w ∧ O v w›..
with ‹¬ O v (σ v. F v)› show "False"..
qed
qed
qed
qed
lemma fusion_part: "F x ⟹ P x (σ x. F x)"
proof -
assume "F x"
hence "∃x. F x"..
hence "∀y. P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"
by (rule fusion_part_character)
hence "P x (σ v. F v) ⟷ (∀w. P w x ⟶ (∃v. F v ∧ O w v))"..
moreover have "∀w. P w x ⟶ (∃v. F v ∧ O w v)"
proof
fix w
show "P w x ⟶ (∃v. F v ∧ O w v)"
proof
assume "P w x"
hence "O w x" by (rule part_implies_overlap)
with ‹F x› have "F x ∧ O w x"..
thus "∃v. F v ∧ O w v"..
qed
qed
ultimately show "P x (σ v. F v)"..
qed
lemma common_part_fusion:
"O x y ⟹ (∀w. P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y))"
proof -
assume "O x y"
with overlap_eq have "∃z. (P z x ∧ P z y)"..
hence sum: "(∀w. P w (σ v. (P v x ∧ P v y)) ⟷
(∀z. P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v)))"
by (rule fusion_part_character)
show "∀w. P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y)"
proof
fix w
from sum have w: "P w (σ v. (P v x ∧ P v y))
⟷ (∀z. P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v))"..
show "P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y)"
proof
assume "P w (σ v. (P v x ∧ P v y))"
with w have bla:
"(∀z. P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v))"..
show "P w x ∧ P w y"
proof
show "P w x"
proof (rule ccontr)
assume "¬ P w x"
hence "∃z. P z w ∧ ¬ O z x"
by (rule strong_supplementation)
then obtain z where z: "P z w ∧ ¬ O z x"..
hence "¬ O z x"..
from bla have "P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v)"..
moreover from z have "P z w"..
ultimately have "∃v. (P v x ∧ P v y) ∧ O z v"..
then obtain v where v: "(P v x ∧ P v y) ∧ O z v"..
hence "P v x ∧ P v y"..
hence "P v x"..
moreover from v have "O z v"..
ultimately have "O z x"
by (rule overlap_monotonicity)
with ‹¬ O z x› show "False"..
qed
show "P w y"
proof (rule ccontr)
assume "¬ P w y"
hence "∃z. P z w ∧ ¬ O z y"
by (rule strong_supplementation)
then obtain z where z: "P z w ∧ ¬ O z y"..
hence "¬ O z y"..
from bla have "P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v)"..
moreover from z have "P z w"..
ultimately have "∃v. (P v x ∧ P v y) ∧ O z v"..
then obtain v where v: "(P v x ∧ P v y) ∧ O z v"..
hence "P v x ∧ P v y"..
hence "P v y"..
moreover from v have "O z v"..
ultimately have "O z y"
by (rule overlap_monotonicity)
with ‹¬ O z y› show "False"..
qed
qed
next
assume "P w x ∧ P w y"
thus "P w (σ v. (P v x ∧ P v y))"
by (rule fusion_part)
qed
qed
qed
theorem product_closure:
"O x y ⟹ (∃z. ∀w. P w z ⟷ (P w x ∧ P w y))"
proof -
assume "O x y"
hence "(∀w. P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y))"
by (rule common_part_fusion)
thus "∃z. ∀w. P w z ⟷ (P w x ∧ P w y)"..
qed
end
sublocale GEM ⊆ CEM
proof
fix x y
show "∃z. ∀w. O w z = (O w x ∨ O w y)"
using sum_closure.
show "x ⊕ y = (THE z. ∀v. O v z ⟷ O v x ∨ O v y)"
using sum_eq.
show "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)"
using product_eq.
show "O x y ⟹ (∃z. ∀w. P w z = (P w x ∧ P w y))"
using product_closure.
qed
context GEM
begin
corollary "O x y ⟹ x ⊗ y = (σ v. P v x ∧ P v y)"
proof -
assume "O x y"
hence "(∀w. P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y))"
by (rule common_part_fusion)
thus "x ⊗ y = (σ v. P v x ∧ P v y)" by (rule product_intro)
qed
lemma disjoint_fusion:
"∃w. ¬ O w x ⟹ (∀w. P w (σ z. ¬ O z x) ⟷ ¬ O w x)"
proof -
assume antecedent: "∃w. ¬ O w x"
hence "∀y. O y (σ v. ¬ O v x) ⟷ (∃v. ¬ O v x ∧ O y v)"
by (rule fusion_character)
hence x: "O x (σ v. ¬ O v x) ⟷ (∃v. ¬ O v x ∧ O x v)"..
show "∀w. P w (σ z. ¬ O z x) ⟷ ¬ O w x"
proof
fix y
show "P y (σ z. ¬ O z x) ⟷ ¬ O y x"
proof
assume "P y (σ z. ¬ O z x)"
moreover have "¬ O x (σ z. ¬ O z x)"
proof
assume "O x (σ z. ¬ O z x)"
with x have "(∃v. ¬ O v x ∧ O x v)"..
then obtain v where v: "¬ O v x ∧ O x v"..
hence "¬ O v x"..
from v have "O x v"..
hence "O v x" by (rule overlap_symmetry)
with ‹¬ O v x› show "False"..
qed
ultimately have "¬ O x y"
by (rule disjoint_demonotonicity)
thus "¬ O y x" by (rule disjoint_symmetry)
next
assume "¬ O y x"
thus "P y (σ v. ¬ O v x)"
by (rule fusion_part)
qed
qed
qed
theorem complement_closure:
"∃w. ¬ O w x ⟹ (∃z. ∀w. P w z ⟷ ¬ O w x)"
proof -
assume "(∃w. ¬ O w x)"
hence "∀w. P w (σ z. ¬ O z x) ⟷ ¬ O w x"
by (rule disjoint_fusion)
thus "∃z. ∀w. P w z ⟷ ¬ O w x"..
qed
end
sublocale GEM ⊆ CEMC
proof
fix x y
show "─ x = (THE z. ∀w. P w z ⟷ ¬ O w x)"
using complement_eq.
show "(∃w. ¬ O w x) ⟹ (∃z. ∀w. P w z = (¬ O w x))"
using complement_closure.
show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))"
using difference_eq.
show "u = (THE x. ∀y. P y x)"
using universe_eq.
qed
context GEM
begin
corollary complement_is_disjoint_fusion:
"∃w. ¬ O w x ⟹ ─ x = (σ z. ¬ O z x)"
proof -
assume "∃w. ¬ O w x"
hence "∀w. P w (σ z. ¬ O z x) ⟷ ¬ O w x"
by (rule disjoint_fusion)
thus "─ x = (σ z. ¬ O z x)"
by (rule complement_intro)
qed
theorem strong_fusion: "∃x. F x ⟹
∃x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
proof -
assume "∃x. F x"
have "(∀y. F y ⟶ P y (σ v. F v)) ∧
(∀y. P y (σ v. F v) ⟶ (∃z. F z ∧ O y z))"
proof
show "∀y. F y ⟶ P y (σ v. F v)"
proof
fix y
show "F y ⟶ P y (σ v. F v)"
proof
assume "F y"
thus "P y (σ v. F v)"
by (rule fusion_part)
qed
qed
next
have "(∀y. P y (σ v. F v) ⟷
(∀w. P w y ⟶ (∃v. F v ∧ O w v)))"
using ‹∃x. F x› by (rule fusion_part_character)
hence "P (σ v. F v) (σ v. F v) ⟷ (∀w. P w (σ v. F v) ⟶
(∃v. F v ∧ O w v))"..
thus "∀w. P w (σ v. F v) ⟶ (∃v. F v ∧ O w v)" using part_reflexivity..
qed
thus ?thesis..
qed
theorem strong_fusion_eq: "∃x. F x ⟹ (σ x. F x) =
(THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))"
proof -
assume "∃x. F x"
have "(THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))) = (σ x. F x)"
proof (rule the_equality)
show "(∀y. F y ⟶ P y (σ x. F x)) ∧ (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z))"
proof
show "∀y. F y ⟶ P y (σ x. F x)"
proof
fix y
show "F y ⟶ P y (σ x. F x)"
proof
assume "F y"
thus "P y (σ x. F x)"
by (rule fusion_part)
qed
qed
next
show "(∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z))"
proof
fix y
show "P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)"
proof
have "∀y. P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"
using ‹∃x. F x› by (rule fusion_part_character)
hence "P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"..
moreover assume "P y (σ x. F x)"
ultimately have "∀w. P w y ⟶ (∃v. F v ∧ O w v)"..
hence "P y y ⟶ (∃v. F v ∧ O y v)"..
thus "∃v. F v ∧ O y v" using part_reflexivity..
qed
qed
qed
next
fix x
assume x: "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
have "∀y. O y x ⟷ (∃z. F z ∧ O y z)"
proof
fix y
show "O y x ⟷ (∃z. F z ∧ O y z)"
proof
assume "O y x"
with overlap_eq have "∃v. P v y ∧ P v x"..
then obtain v where v: "P v y ∧ P v x"..
from x have "∀y. P y x ⟶ (∃z. F z ∧ O y z)"..
hence "P v x ⟶ (∃z. F z ∧ O v z)"..
moreover from v have "P v x"..
ultimately have "∃z. F z ∧ O v z"..
then obtain z where z: "F z ∧ O v z"..
hence "F z"..
from v have "P v y"..
moreover from z have "O v z"..
hence "O z v" by (rule overlap_symmetry)
ultimately have "O z y" by (rule overlap_monotonicity)
hence "O y z" by (rule overlap_symmetry)
with ‹F z› have "F z ∧ O y z"..
thus "∃z. F z ∧ O y z"..
next
assume "∃z. F z ∧ O y z"
then obtain z where z: "F z ∧ O y z"..
from x have "∀y. F y ⟶ P y x"..
hence "F z ⟶ P z x"..
moreover from z have "F z"..
ultimately have "P z x"..
moreover from z have "O y z"..
ultimately show "O y x"
by (rule overlap_monotonicity)
qed
qed
hence "(σ x. F x) = x"
by (rule fusion_intro)
thus "x = (σ x. F x)"..
qed
thus ?thesis..
qed
lemma strong_sum_eq: "x ⊕ y = (THE z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y))"
proof -
have "(THE z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)) = x ⊕ y"
proof (rule the_equality)
show "(P x (x ⊕ y) ∧ P y (x ⊕ y)) ∧ (∀w. P w (x ⊕ y) ⟶ O w x ∨ O w y)"
proof
show "P x (x ⊕ y) ∧ P y (x ⊕ y)"
proof
show "P x (x ⊕ y)" using first_summand_in_sum.
show "P y (x ⊕ y)" using second_summand_in_sum.
qed
show "∀w. P w (x ⊕ y) ⟶ O w x ∨ O w y"
proof
fix w
show "P w (x ⊕ y) ⟶ O w x ∨ O w y"
proof
assume "P w (x ⊕ y)"
hence "O w (x ⊕ y)" by (rule part_implies_overlap)
with sum_overlap show "O w x ∨ O w y"..
qed
qed
qed
fix z
assume z: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
hence "P x z ∧ P y z"..
have "∀w. O w z ⟷ (O w x ∨ O w y)"
proof
fix w
show "O w z ⟷ (O w x ∨ O w y)"
proof
assume "O w z"
with overlap_eq have "∃v. P v w ∧ P v z"..
then obtain v where v: "P v w ∧ P v z"..
hence "P v w"..
from z have "∀w. P w z ⟶ O w x ∨ O w y"..
hence "P v z ⟶ O v x ∨ O v y"..
moreover from v have "P v z"..
ultimately have "O v x ∨ O v y"..
thus "O w x ∨ O w y"
proof
assume "O v x"
hence "O x v" by (rule overlap_symmetry)
with ‹P v w› have "O x w" by (rule overlap_monotonicity)
hence "O w x" by (rule overlap_symmetry)
thus "O w x ∨ O w y"..
next
assume "O v y"
hence "O y v" by (rule overlap_symmetry)
with ‹P v w› have "O y w" by (rule overlap_monotonicity)
hence "O w y" by (rule overlap_symmetry)
thus "O w x ∨ O w y"..
qed
next
assume "O w x ∨ O w y"
thus "O w z"
proof
from ‹P x z ∧ P y z› have "P x z"..
moreover assume "O w x"
ultimately show "O w z"
by (rule overlap_monotonicity)
next
from ‹P x z ∧ P y z› have "P y z"..
moreover assume "O w y"
ultimately show "O w z"
by (rule overlap_monotonicity)
qed
qed
qed
hence "x ⊕ y = z" by (rule sum_intro)
thus "z = x ⊕ y"..
qed
thus ?thesis..
qed
subsection ‹ General Products ›
lemma general_product_intro: "(∀y. O y x ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z)) ⟹ (π x. F x) = x"
proof -
assume "∀y. O y x ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z)"
hence "(σ x. ∀y. F y ⟶ P x y) = x" by (rule fusion_intro)
with general_product_eq show "(π x. F x) = x" by (rule ssubst)
qed
lemma general_product_idempotence: "(π z. z = x) = x"
proof -
have "∀y. O y x ⟷ (∃z. (∀y. y = x ⟶ P z y) ∧ O y z)"
by (meson overlap_eq part_reflexivity part_transitivity)
thus "(π z. z = x) = x" by (rule general_product_intro)
qed
lemma general_product_absorption: "(π z. P x z) = x"
proof -
have "∀y. O y x ⟷ (∃z. (∀y. P x y ⟶ P z y) ∧ O y z)"
by (meson overlap_eq part_reflexivity part_transitivity)
thus "(π z. P x z) = x" by (rule general_product_intro)
qed
lemma general_product_character: "∃z. ∀y. F y ⟶ P z y ⟹
∀y. O y (π x. F x) ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z)"
proof -
assume "(∃z. ∀y. F y ⟶ P z y)"
hence "(∃x. ∀y. O y x ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z))"
by (rule fusion)
then obtain x where x:
"∀y. O y x ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z)"..
hence "(π x. F x) = x" by (rule general_product_intro)
thus "(∀y. O y (π x. F x) ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z))"
using x by (rule ssubst)
qed
corollary "¬ (∃x. F x) ⟹ u = (π x. F x)"
proof -
assume antecedent: "¬ (∃x. F x)"
have "∀y. P y (π x. F x)"
proof
fix y
show "P y (π x. F x)"
proof (rule ccontr)
assume "¬ P y (π x. F x)"
hence "∃z. P z y ∧ ¬ O z (π x. F x)" by (rule strong_supplementation)
then obtain z where z: "P z y ∧ ¬ O z (π x. F x)"..
hence "¬ O z (π x. F x)"..
from antecedent have bla: "∀ y. F y ⟶ P z y" by simp
hence "∃ v. ∀ y. F y ⟶ P v y"..
hence "(∀y. O y (π x. F x) ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z))" by (rule general_product_character)
hence "O z (π x. F x) ⟷ (∃v. (∀y. F y ⟶ P v y) ∧ O z v)"..
moreover from bla have "(∀ y. F y ⟶ P z y) ∧ O z z"
using overlap_reflexivity..
hence "∃ v. (∀ y. F y ⟶ P v y) ∧ O z v"..
ultimately have "O z (π x. F x)"..
with ‹¬ O z (π x. F x)› show "False"..
qed
qed
thus "u = (π x. F x)"
by (rule universe_intro)
qed
end
subsection ‹ Strong Fusion ›
text ‹ An alternative axiomatization of general extensional mereology adds a stronger version of the
fusion axiom to minimal mereology, with correspondingly stronger definitions of sums and general
sums.\footnote{See \<^cite>‹"tarski_foundations_1983"› p. 25. The proofs in this section are adapted
from \<^cite>‹"hovda_what_2009"›.} ›
locale GEM1 = MM +
assumes strong_fusion: "∃x. F x ⟹ ∃x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
assumes strong_sum_eq: "x ⊕ y = (THE z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y))"
assumes product_eq:
"x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)"
assumes difference_eq:
"x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))"
assumes complement_eq: "─ x = (THE z. ∀w. P w z ⟷ ¬ O w x)"
assumes universe_eq: "u = (THE x. ∀y. P y x)"
assumes strong_fusion_eq: "∃x. F x ⟹ (σ x. F x) = (THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))"
assumes general_product_eq: "(π x. F x) = (σ x. ∀y. F y ⟶ P x y)"
begin
theorem fusion:
"∃x. φ x ⟹ (∃z. ∀y. O y z ⟷ (∃x. φ x ∧ O y x))"
proof -
assume "∃x. φ x"
hence "∃x. (∀y. φ y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. φ z ∧ O y z))" by (rule strong_fusion)
then obtain x where x:
"(∀y. φ y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. φ z ∧ O y z))"..
have "∀y. O y x ⟷ (∃v. φ v ∧ O y v)"
proof
fix y
show "O y x ⟷ (∃v. φ v ∧ O y v)"
proof
assume "O y x"
with overlap_eq have "∃z. P z y ∧ P z x"..
then obtain z where z: "P z y ∧ P z x"..
hence "P z x"..
from x have "∀y. P y x ⟶ (∃v. φ v ∧ O y v)"..
hence "P z x ⟶ (∃v. φ v ∧ O z v)"..
hence "∃v. φ v ∧ O z v" using ‹P z x›..
then obtain v where v: "φ v ∧ O z v"..
hence "O z v"..
with overlap_eq have "∃w. P w z ∧ P w v"..
then obtain w where w: "P w z ∧ P w v"..
hence "P w z"..
moreover from z have "P z y"..
ultimately have "P w y"
by (rule part_transitivity)
moreover from w have "P w v"..
ultimately have "P w y ∧ P w v"..
hence "∃w. P w y ∧ P w v"..
with overlap_eq have "O y v"..
from v have "φ v"..
hence "φ v ∧ O y v" using ‹O y v›..
thus "∃v. φ v ∧ O y v"..
next
assume "∃v. φ v ∧ O y v"
then obtain v where v: "φ v ∧ O y v"..
hence "O y v"..
with overlap_eq have "∃z. P z y ∧ P z v"..
then obtain z where z: "P z y ∧ P z v"..
hence "P z v"..
from x have "∀y. φ y ⟶ P y x"..
hence "φ v ⟶ P v x"..
moreover from v have "φ v"..
ultimately have "P v x"..
with ‹P z v› have "P z x"
by (rule part_transitivity)
from z have "P z y"..
thus "O y x" using ‹P z x›
by (rule overlap_intro)
qed
qed
thus "(∃z. ∀y. O y z ⟷ (∃x. φ x ∧ O y x))"..
qed
lemma pair: "∃v. (∀w. (w = x ∨ w = y) ⟶ P w v) ∧ (∀w. P w v ⟶ (∃z. (z = x ∨ z = y) ∧ O w z))"
proof -
have "x = x"..
hence "x = x ∨ x = y"..
hence "∃v. v = x ∨ v = y"..
thus ?thesis
by (rule strong_fusion)
qed
lemma or_id: "(v = x ∨ v = y) ∧ O w v ⟹ O w x ∨ O w y"
proof -
assume v: "(v = x ∨ v = y) ∧ O w v"
hence "O w v"..
from v have "v = x ∨ v = y"..
thus "O w x ∨ O w y"
proof
assume "v = x"
hence "O w x" using ‹O w v› by (rule subst)
thus "O w x ∨ O w y"..
next
assume "v = y"
hence "O w y" using ‹O w v› by (rule subst)
thus "O w x ∨ O w y"..
qed
qed
lemma strong_sum_closure:
"∃z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
proof -
from pair obtain z where z: "(∀w. (w = x ∨ w = y) ⟶ P w z) ∧ (∀w. P w z ⟶ (∃v. (v = x ∨ v = y) ∧ O w v))"..
have "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
proof
from z have allw: "∀w. (w = x ∨ w = y) ⟶ P w z"..
hence "x = x ∨ x = y ⟶ P x z"..
moreover have "x = x ∨ x = y" using refl..
ultimately have "P x z"..
from allw have "y = x ∨ y = y ⟶ P y z"..
moreover have "y = x ∨ y = y" using refl..
ultimately have "P y z"..
with ‹P x z› show "P x z ∧ P y z"..
next
show "∀w. P w z ⟶ O w x ∨ O w y"
proof
fix w
show "P w z ⟶ O w x ∨ O w y"
proof
assume "P w z"
from z have "∀w. P w z ⟶ (∃v. (v = x ∨ v = y) ∧ O w v)"..
hence "P w z ⟶ (∃v. (v = x ∨ v = y) ∧ O w v)"..
hence "∃v. (v = x ∨ v = y) ∧ O w v" using ‹P w z›..
then obtain v where v: "(v = x ∨ v = y) ∧ O w v"..
thus "O w x ∨ O w y" by (rule or_id)
qed
qed
qed
thus ?thesis..
qed
end
sublocale GEM1 ⊆ GMM
proof
fix x y φ
show "(∃x. φ x) ⟹ (∃z. ∀y. O y z ⟷ (∃x. φ x ∧ O y x))" using fusion.
qed
context GEM1
begin
lemma least_upper_bound:
assumes sf:
"((∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))"
shows lub:
"(∀y. F y ⟶ P y x) ∧ (∀z. (∀y. F y ⟶ P y z) ⟶ P x z)"
proof
from sf show "∀y. F y ⟶ P y x"..
next
show "(∀z. (∀y. F y ⟶ P y z) ⟶ P x z)"
proof
fix z
show "(∀y. F y ⟶ P y z) ⟶ P x z"
proof
assume z: "∀y. F y ⟶ P y z"
from pair obtain v where v: "(∀w. (w = x ∨ w = z) ⟶ P w v) ∧ (∀w. P w v ⟶ (∃y. (y = x ∨ y = z) ∧ O w y))"..
hence left: "(∀w. (w = x ∨ w = z) ⟶ P w v)"..
hence "(x = x ∨ x = z) ⟶ P x v"..
moreover have "x = x ∨ x = z" using refl..
ultimately have "P x v"..
have "z = v"
proof (rule ccontr)
assume "z ≠ v"
from left have "z = x ∨ z = z ⟶ P z v"..
moreover have "z = x ∨ z = z" using refl..
ultimately have "P z v"..
hence "P z v ∧ z ≠ v" using ‹z ≠ v›..
with nip_eq have "PP z v"..
hence "∃w. P w v ∧ ¬ O w z" by (rule weak_supplementation)
then obtain w where w: "P w v ∧ ¬ O w z"..
hence "P w v"..
from v have right:
"∀w. P w v ⟶ (∃y. (y = x ∨ y = z) ∧ O w y)"..
hence "P w v ⟶ (∃y. (y = x ∨ y = z) ∧ O w y)"..
hence "∃y. (y = x ∨ y = z) ∧ O w y" using ‹P w v›..
then obtain s where s: "(s = x ∨ s = z) ∧ O w s"..
hence "s = x ∨ s = z"..
thus "False"
proof
assume "s = x"
moreover from s have "O w s"..
ultimately have "O w x" by (rule subst)
with overlap_eq have "∃t. P t w ∧ P t x"..
then obtain t where t: "P t w ∧ P t x"..
hence "P t x"..
from sf have "(∀y. P y x ⟶ (∃z. F z ∧ O y z))"..
hence "P t x ⟶ (∃z. F z ∧ O t z)"..
hence "∃z. F z ∧ O t z" using ‹P t x›..
then obtain a where a: "F a ∧ O t a"..
hence "F a"..
from sf have ub: "∀y. F y ⟶ P y x"..
hence "F a ⟶ P a x"..
hence "P a x" using ‹F a›..
moreover from a have "O t a"..
ultimately have "O t x"
by (rule overlap_monotonicity)
from t have "P t w"..
moreover have "O z t"
proof -
from z have "F a ⟶ P a z"..
moreover from a have "F a"..
ultimately have "P a z"..
moreover from a have "O t a"..
ultimately have "O t z"
by (rule overlap_monotonicity)
thus "O z t" by (rule overlap_symmetry)
qed
ultimately have "O z w"
by (rule overlap_monotonicity)
hence "O w z" by (rule overlap_symmetry)
from w have "¬ O w z"..
thus "False" using ‹O w z›..
next
assume "s = z"
moreover from s have "O w s"..
ultimately have "O w z" by (rule subst)
from w have "¬ O w z"..
thus "False" using ‹O w z›..
qed
qed
thus "P x z" using ‹P x v› by (rule ssubst)
qed
qed
qed
corollary strong_fusion_intro: "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)) ⟹ (σ x. F x) = x"
proof -
assume antecedent: "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
with least_upper_bound have lubx:
"(∀y. F y ⟶ P y x) ∧ (∀z. (∀y. F y ⟶ P y z) ⟶ P x z)".
from antecedent have "∀y. P y x ⟶ (∃z. F z ∧ O y z)"..
hence "P x x ⟶ (∃z. F z ∧ O x z)"..
hence "∃z. F z ∧ O x z" using part_reflexivity..
then obtain z where z: "F z ∧ O x z"..
hence "F z"..
hence "∃z. F z"..
hence "(σ x. F x) = (THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))" by (rule strong_fusion_eq)
moreover have "(THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))) = x"
proof (rule the_equality)
show "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
using antecedent.
next
fix w
assume w:
"(∀y. F y ⟶ P y w) ∧ (∀y. P y w ⟶ (∃z. F z ∧ O y z))"
with least_upper_bound have lubw:
"(∀y. F y ⟶ P y w) ∧ (∀z. (∀y. F y ⟶ P y z) ⟶ P w z)".
hence "(∀z. (∀y. F y ⟶ P y z) ⟶ P w z)"..
hence "(∀y. F y ⟶ P y x) ⟶ P w x"..
moreover from antecedent have "∀y. F y ⟶ P y x"..
ultimately have "P w x"..
from lubx have "(∀z. (∀y. F y ⟶ P y z) ⟶ P x z)"..
hence "(∀y. F y ⟶ P y w) ⟶ P x w"..
moreover from lubw have "(∀y. F y ⟶ P y w)"..
ultimately have "P x w"..
with ‹P w x› show "w = x"
by (rule part_antisymmetry)
qed
ultimately show "(σ x. F x) = x" by (rule ssubst)
qed
lemma strong_fusion_character: "∃x. F x ⟹ ((∀y. F y ⟶ P y (σ x. F x)) ∧ (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)))"
proof -
assume "∃x. F x"
hence "(∃x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))" by (rule strong_fusion)
then obtain x where x:
"(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"..
hence "(σ x. F x) = x" by (rule strong_fusion_intro)
thus ?thesis using x by (rule ssubst)
qed
lemma F_in: "∃x. F x ⟹ (∀y. F y ⟶ P y (σ x. F x))"
proof -
assume "∃x. F x"
hence "((∀y. F y ⟶ P y (σ x. F x)) ∧ (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)))" by (rule strong_fusion_character)
thus "∀y. F y ⟶ P y (σ x. F x)"..
qed
lemma parts_overlap_Fs:
"∃x. F x ⟹ (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z))"
proof -
assume "∃x. F x"
hence "((∀y. F y ⟶ P y (σ x. F x)) ∧ (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)))" by (rule strong_fusion_character)
thus "(∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z))"..
qed
lemma in_strong_fusion: "P z (σ x. z = x)"
proof -
have "∃y. z = y" using refl..
hence "∀y. z = y ⟶ P y (σ x. z = x)"
by (rule F_in)
hence "z = z ⟶ P z (σ x. z = x)"..
thus "P z (σ x. z = x)" using refl..
qed
lemma strong_fusion_in: "P (σ x. z = x) z"
proof -
have "∃y. z = y" using refl..
hence sf:
"(∀y. z = y ⟶ P y (σ x. z = x)) ∧ (∀y. P y (σ x. z = x) ⟶ (∃v. z = v ∧ O y v))"
by (rule strong_fusion_character)
with least_upper_bound have lub: "(∀y. z = y ⟶ P y (σ x. z = x)) ∧ (∀v. (∀y. z = y ⟶ P y v) ⟶ P (σ x. z = x) v)".
hence "(∀v. (∀y. z = y ⟶ P y v) ⟶ P (σ x. z = x) v)"..
hence "(∀y. z = y ⟶ P y z) ⟶ P (σ x. z = x) z"..
moreover have "(∀y. z = y ⟶ P y z)"
proof
fix y
show "z = y ⟶ P y z"
proof
assume "z = y"
thus "P y z" using part_reflexivity by (rule subst)
qed
qed
ultimately show "P (σ x. z = x) z"..
qed
lemma strong_fusion_idempotence: "(σ x. z = x) = z"
using strong_fusion_in in_strong_fusion by (rule part_antisymmetry)
subsection ‹ Strong Sums ›
lemma pair_fusion: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y) ⟶ (σ z. z = x ∨ z = y) = z"
proof
assume z: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
have "(∀v. v = x ∨ v = y ⟶ P v z) ∧ (∀v. P v z ⟶ (∃z. (z = x ∨ z = y) ∧ O v z))"
proof
show "∀v. v = x ∨ v = y ⟶ P v z"
proof
fix w
from z have "P x z ∧ P y z"..
show "w = x ∨ w = y ⟶ P w z"
proof
assume "w = x ∨ w = y"
thus "P w z"
proof
assume "w = x"
moreover from ‹P x z ∧ P y z› have "P x z"..
ultimately show "P w z" by (rule ssubst)
next
assume "w = y"
moreover from ‹P x z ∧ P y z› have "P y z"..
ultimately show "P w z" by (rule ssubst)
qed
qed
qed
show "∀v. P v z ⟶ (∃z. (z = x ∨ z = y) ∧ O v z)"
proof
fix v
show "P v z ⟶ (∃z. (z = x ∨ z = y) ∧ O v z)"
proof
assume "P v z"
from z have "∀w. P w z ⟶ O w x ∨ O w y"..
hence "P v z ⟶ O v x ∨ O v y"..
hence "O v x ∨ O v y" using ‹P v z›..
thus "∃z. (z = x ∨ z = y) ∧ O v z"
proof
assume "O v x"
have "x = x ∨ x = y" using refl..
hence "(x = x ∨ x = y) ∧ O v x" using ‹O v x›..
thus "∃z. (z = x ∨ z = y) ∧ O v z"..
next
assume "O v y"
have "y = x ∨ y = y" using refl..
hence "(y = x ∨ y = y) ∧ O v y" using ‹O v y›..
thus "∃z. (z = x ∨ z = y) ∧ O v z"..
qed
qed
qed
qed
thus "(σ z. z = x ∨ z = y) = z"
by (rule strong_fusion_intro)
qed
corollary strong_sum_fusion: "x ⊕ y = (σ z. z = x ∨ z = y)"
proof -
have "(THE z. (P x z ∧ P y z) ∧
(∀w. P w z ⟶ O w x ∨ O w y)) = (σ z. z = x ∨ z = y)"
proof (rule the_equality)
have "x = x ∨ x = y" using refl..
hence exz: "∃z. z = x ∨ z = y"..
hence allw: "(∀w. w = x ∨ w = y ⟶ P w (σ z. z = x ∨ z = y))"
by (rule F_in)
show "(P x (σ z. z = x ∨ z = y) ∧ P y (σ z. z = x ∨ z = y)) ∧
(∀w. P w (σ z. z = x ∨ z = y) ⟶ O w x ∨ O w y)"
proof
show "(P x (σ z. z = x ∨ z = y) ∧ P y (σ z. z = x ∨ z = y))"
proof
from allw have "x = x ∨ x = y ⟶ P x (σ z. z = x ∨ z = y)"..
thus "P x (σ z. z = x ∨ z = y)"
using ‹x = x ∨ x = y›..
next
from allw have "y = x ∨ y = y ⟶ P y (σ z. z = x ∨ z = y)"..
moreover have "y = x ∨ y = y"
using refl..
ultimately show "P y (σ z. z = x ∨ z = y)"..
qed
next
show "∀w. P w (σ z. z = x ∨ z = y) ⟶ O w x ∨ O w y"
proof
fix w
show "P w (σ z. z = x ∨ z = y) ⟶ O w x ∨ O w y"
proof
have "∀v. P v (σ z. z = x ∨ z = y) ⟶ (∃z. (z = x ∨ z = y) ∧ O v z)" using exz by (rule parts_overlap_Fs)
hence "P w (σ z. z = x ∨ z = y) ⟶ (∃z. (z = x ∨ z = y) ∧ O w z)"..
moreover assume "P w (σ z. z = x ∨ z = y)"
ultimately have "(∃z. (z = x ∨ z = y) ∧ O w z)"..
then obtain z where z: "(z = x ∨ z = y) ∧ O w z"..
thus "O w x ∨ O w y" by (rule or_id)
qed
qed
qed
next
fix z
assume z: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
with pair_fusion have "(σ z. z = x ∨ z = y) = z"..
thus "z = (σ z. z = x ∨ z = y)"..
qed
with strong_sum_eq show "x ⊕ y = (σ z. z = x ∨ z = y)"
by (rule ssubst)
qed
corollary strong_sum_intro:
"(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y) ⟶ x ⊕ y = z"
proof
assume z: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
with pair_fusion have "(σ z. z = x ∨ z = y) = z"..
with strong_sum_fusion show "(x ⊕ y) = z"
by (rule ssubst)
qed
corollary strong_sum_character: "(P x (x ⊕ y) ∧ P y (x ⊕ y)) ∧ (∀w. P w (x ⊕ y) ⟶ O w x ∨ O w y)"
proof -
from strong_sum_closure obtain z where z:
"(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"..
with strong_sum_intro have "x ⊕ y = z"..
thus ?thesis using z by (rule ssubst)
qed
corollary summands_in: "(P x (x ⊕ y) ∧ P y (x ⊕ y))"
using strong_sum_character..
corollary first_summand_in: "P x (x ⊕ y)" using summands_in..
corollary second_summand_in: "P y (x ⊕ y)" using summands_in..
corollary sum_part_overlap: "(∀w. P w (x ⊕ y) ⟶ O w x ∨ O w y)" using strong_sum_character..
lemma strong_sum_absorption: "y = (x ⊕ y) ⟹ P x y"
proof -
assume "y = (x ⊕ y)"
thus "P x y" using first_summand_in by (rule ssubst)
qed
theorem strong_supplementation: "¬ P x y ⟹ (∃z. P z x ∧ ¬ O z y)"
proof -
assume "¬ P x y"
have "¬ (∀z. P z x ⟶ O z y)"
proof
assume z: "∀z. P z x ⟶ O z y"
have "(∀v. y = v ⟶ P v (x ⊕ y)) ∧
(∀v. P v (x ⊕ y) ⟶ (∃z. y = z ∧ O v z))"
proof
show "∀v. y = v ⟶ P v (x ⊕ y)"
proof
fix v
show "y = v ⟶ P v (x ⊕ y)"
proof
assume "y = v"
thus "P v (x ⊕ y)"
using second_summand_in by (rule subst)
qed
qed
show "∀v. P v (x ⊕ y) ⟶ (∃z. y = z ∧ O v z)"
proof
fix v
show "P v (x ⊕ y) ⟶ (∃z. y = z ∧ O v z)"
proof
assume "P v (x ⊕ y)"
moreover from sum_part_overlap have
"P v (x ⊕ y) ⟶ O v x ∨ O v y"..
ultimately have "O v x ∨ O v y" by (rule rev_mp)
hence "O v y"
proof
assume "O v x"
with overlap_eq have "∃w. P w v ∧ P w x"..
then obtain w where w: "P w v ∧ P w x"..
from z have "P w x ⟶ O w y"..
moreover from w have "P w x"..
ultimately have "O w y"..
with overlap_eq have "∃t. P t w ∧ P t y"..
then obtain t where t: "P t w ∧ P t y"..
hence "P t w"..
moreover from w have "P w v"..
ultimately have "P t v"
by (rule part_transitivity)
moreover from t have "P t y"..
ultimately show "O v y"
by (rule overlap_intro)
next
assume "O v y"
thus "O v y".
qed
with refl have "y = y ∧ O v y"..
thus "∃z. y = z ∧ O v z"..
qed
qed
qed
hence "(σ z. y = z) = (x ⊕ y)" by (rule strong_fusion_intro)
with strong_fusion_idempotence have "y = x ⊕ y" by (rule subst)
hence "P x y" by (rule strong_sum_absorption)
with ‹¬ P x y› show "False"..
qed
thus "∃z. P z x ∧ ¬ O z y" by simp
qed
lemma sum_character: "∀v. O v (x ⊕ y) ⟷ (O v x ∨ O v y)"
proof
fix v
show "O v (x ⊕ y) ⟷ (O v x ∨ O v y)"
proof
assume "O v (x ⊕ y)"
with overlap_eq have "∃w. P w v ∧ P w (x ⊕ y)"..
then obtain w where w: "P w v ∧ P w (x ⊕ y)"..
hence "P w v"..
have "P w (x ⊕ y) ⟶ O w x ∨ O w y" using sum_part_overlap..
moreover from w have "P w (x ⊕ y)"..
ultimately have "O w x ∨ O w y"..
thus "O v x ∨ O v y"
proof
assume "O w x"
hence "O x w"
by (rule overlap_symmetry)
with ‹P w v› have "O x v"
by (rule overlap_monotonicity)
hence "O v x"
by (rule overlap_symmetry)
thus "O v x ∨ O v y"..
next
assume "O w y"
hence "O y w"
by (rule overlap_symmetry)
with ‹P w v› have "O y v"
by (rule overlap_monotonicity)
hence "O v y" by (rule overlap_symmetry)
thus "O v x ∨ O v y"..
qed
next
assume "O v x ∨ O v y"
thus "O v (x ⊕ y)"
proof
assume "O v x"
with overlap_eq have "∃w. P w v ∧ P w x"..
then obtain w where w: "P w v ∧ P w x"..
hence "P w v"..
moreover from w have "P w x"..
hence "P w (x ⊕ y)" using first_summand_in
by (rule part_transitivity)
ultimately show "O v (x ⊕ y)"
by (rule overlap_intro)
next
assume "O v y"
with overlap_eq have "∃w. P w v ∧ P w y"..
then obtain w where w: "P w v ∧ P w y"..
hence "P w v"..
moreover from w have "P w y"..
hence "P w (x ⊕ y)" using second_summand_in
by (rule part_transitivity)
ultimately show "O v (x ⊕ y)"
by (rule overlap_intro)
qed
qed
qed
lemma sum_eq: "x ⊕ y = (THE z. ∀v. O v z = (O v x ∨ O v y))"
proof -
have "(THE z. ∀v. O v z ⟷ (O v x ∨ O v y)) = x ⊕ y"
proof (rule the_equality)
show "∀v. O v (x ⊕ y) ⟷ (O v x ∨ O v y)" using sum_character.
next
fix z
assume z: "∀v. O v z ⟷ (O v x ∨ O v y)"
have "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
proof
show "P x z ∧ P y z"
proof
show "P x z"
proof (rule ccontr)
assume "¬ P x z"
hence "∃v. P v x ∧ ¬ O v z"
by (rule strong_supplementation)
then obtain v where v: "P v x ∧ ¬ O v z"..
hence "¬ O v z"..
from z have "O v z ⟷ (O v x ∨ O v y)"..
moreover from v have "P v x"..
hence "O v x" by (rule part_implies_overlap)
hence "O v x ∨ O v y"..
ultimately have "O v z"..
with ‹¬ O v z› show "False"..
qed
next
show "P y z"
proof (rule ccontr)
assume "¬ P y z"
hence "∃v. P v y ∧ ¬ O v z"
by (rule strong_supplementation)
then obtain v where v: "P v y ∧ ¬ O v z"..
hence "¬ O v z"..
from z have "O v z ⟷ (O v x ∨ O v y)"..
moreover from v have "P v y"..
hence "O v y" by (rule part_implies_overlap)
hence "O v x ∨ O v y"..
ultimately have "O v z"..
with ‹¬ O v z› show "False"..
qed
qed
show "∀w. P w z ⟶ (O w x ∨ O w y)"
proof
fix w
show "P w z ⟶ (O w x ∨ O w y)"
proof
from z have "O w z ⟷ O w x ∨ O w y"..
moreover assume "P w z"
hence "O w z" by (rule part_implies_overlap)
ultimately show "O w x ∨ O w y"..
qed
qed
qed
with strong_sum_intro have "x ⊕ y = z"..
thus "z = x ⊕ y"..
qed
thus ?thesis..
qed
theorem fusion_eq: "∃x. F x ⟹
(σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))"
proof -
assume "∃x. F x"
hence bla: "∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)"
by (rule parts_overlap_Fs)
have "(THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z)) = (σ x. F x)"
proof (rule the_equality)
show "∀y. O y (σ x. F x) ⟷ (∃z. F z ∧ O y z)"
proof
fix y
show "O y (σ x. F x) ⟷ (∃z. F z ∧ O y z)"
proof
assume "O y (σ x. F x)"
with overlap_eq have "∃v. P v y ∧ P v (σ x. F x)"..
then obtain v where v: "P v y ∧ P v (σ x. F x)"..
hence "P v y"..
from bla have "P v (σ x. F x) ⟶ (∃z. F z ∧ O v z)"..
moreover from v have "P v (σ x. F x)"..
ultimately have "(∃z. F z ∧ O v z)"..
then obtain z where z: "F z ∧ O v z"..
hence "F z"..
moreover from z have "O v z"..
hence "O z v" by (rule overlap_symmetry)
with ‹P v y› have "O z y" by (rule overlap_monotonicity)
hence "O y z" by (rule overlap_symmetry)
ultimately have "F z ∧ O y z"..
thus "(∃z. F z ∧ O y z)"..
next
assume "∃z. F z ∧ O y z"
then obtain z where z: "F z ∧ O y z"..
from‹∃x. F x› have "(∀y. F y ⟶ P y (σ x. F x))"
by (rule F_in)
hence "F z ⟶ P z (σ x. F x)"..
moreover from z have "F z"..
ultimately have "P z (σ x. F x)"..
moreover from z have "O y z"..
ultimately show "O y (σ x. F x)"
by (rule overlap_monotonicity)
qed
qed
next
fix x
assume x: "∀y. O y x ⟷ (∃v. F v ∧ O y v)"
have "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
proof
show "∀y. F y ⟶ P y x"
proof
fix y
show "F y ⟶ P y x"
proof
assume "F y"
show "P y x"
proof (rule ccontr)
assume "¬ P y x"
hence "∃z. P z y ∧ ¬ O z x"
by (rule strong_supplementation)
then obtain z where z: "P z y ∧ ¬ O z x"..
hence "¬ O z x"..
from x have "O z x ⟷ (∃v. F v ∧ O z v)"..
moreover from z have "P z y"..
hence "O z y" by (rule part_implies_overlap)
with ‹F y› have "F y ∧ O z y"..
hence "∃y. F y ∧ O z y"..
ultimately have "O z x"..
with ‹¬ O z x› show "False"..
qed
qed
qed
show "∀y. P y x ⟶ (∃z. F z ∧ O y z)"
proof
fix y
show "P y x ⟶ (∃z. F z ∧ O y z)"
proof
from x have "O y x ⟷ (∃z. F z ∧ O y z)"..
moreover assume "P y x"
hence "O y x" by (rule part_implies_overlap)
ultimately show "∃z. F z ∧ O y z"..
qed
qed
qed
hence "(σ x. F x) = x"
by (rule strong_fusion_intro)
thus "x = (σ x. F x)"..
qed
thus "(σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))"..
qed
end
sublocale GEM1 ⊆ GEM
proof
fix x y F
show "¬ P x y ⟹ ∃z. P z x ∧ ¬ O z y"
using strong_supplementation.
show "x ⊕ y = (THE z. ∀v. O v z ⟷ (O v x ∨ O v y))"
using sum_eq.
show "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)"
using product_eq.
show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))"
using difference_eq.
show "─ x = (THE z. ∀w. P w z ⟷ ¬ O w x)"
using complement_eq.
show "u = (THE x. ∀y. P y x)"
using universe_eq.
show "∃x. F x ⟹ (σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))" using fusion_eq.
show "(π x. F x) = (σ x. ∀y. F y ⟶ P x y)"
using general_product_eq.
qed
sublocale GEM ⊆ GEM1
proof
fix x y F
show "∃x. F x ⟹ (∃x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))" using strong_fusion.
show "∃x. F x ⟹ (σ x. F x) = (THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))" using strong_fusion_eq.
show "(π x. F x) = (σ x. ∀y. F y ⟶ P x y)" using general_product_eq.
show "x ⊕ y = (THE z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y))" using strong_sum_eq.
show "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)"
using product_eq.
show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))"
using difference_eq.
show "─ x = (THE z. ∀w. P w z ⟷ ¬ O w x)" using complement_eq.
show "u = (THE x. ∀y. P y x)" using universe_eq.
qed
end