Commit 1d78b0b5 authored by nipkow's avatar nipkow
Browse files

New entry: Mereology

parent 5308f917cbab
......@@ -10323,3 +10323,13 @@ abstract =
<i>(r - 1)<sup>k</sup> &middot; k!</i>,
then it contains a sunflower of cardinality <i>r</i>.
 
[Mereology]
title = Mereology
author = Ben Blumson <https://philpeople.org/profiles/ben-blumson>
topic = Logic/Philosophical aspects
date = 2021-03-01
notify = benblumson@gmail.com
abstract =
We use Isabelle/HOL to verify elementary theorems and alternative
axiomatizations of classical extensional mereology.
This diff is collapsed.
This diff is collapsed.
section \<open> Extensional Mereology \<close>
(*<*)
theory EM
imports MM
begin
(*>*)
text \<open> Extensional mereology adds to ground mereology the axiom of strong supplementation.\footnote{
See @{cite "simons_parts:_1987"} p. 29, @{cite "varzi_parts_1996"} p. 262 and @{cite "casati_parts_1999"}
p. 39-40.} \<close>
locale EM = M +
assumes strong_supplementation:
"\<not> P x y \<Longrightarrow> (\<exists>z. P z x \<and> \<not> O z y)"
begin
text \<open> Strong supplementation entails weak supplementation.\footnote{See @{cite "simons_parts:_1987"}
p. 29 and @{cite "casati_parts_1999"} p. 40.} \<close>
lemma weak_supplementation: "PP x y \<Longrightarrow> (\<exists>z. P z y \<and> \<not> O z x)"
proof -
assume "PP x y"
hence "\<not> P y x" by (rule proper_implies_not_part)
thus "\<exists>z. P z y \<and> \<not> O z x" by (rule strong_supplementation)
qed
end
text \<open> So minimal mereology is a subtheory of extensional mereology.\footnote{@{cite "casati_parts_1999"} p. 40.} \<close>
sublocale EM \<subseteq> MM
proof
fix y x
show "PP y x \<Longrightarrow> \<exists>z. P z x \<and> \<not> O z y" using weak_supplementation.
qed
text \<open> Strong supplementation also entails the proper parts principle.\footnote{See @{cite "simons_parts:_1987"}
pp. 28-9 and @{cite "varzi_parts_1996"} p. 263.} \<close>
context EM
begin
lemma proper_parts_principle:
"(\<exists>z. PP z x) \<Longrightarrow> (\<forall>z. PP z x \<longrightarrow> P z y) \<Longrightarrow> P x y"
proof -
assume "\<exists>z. PP z x"
then obtain v where v: "PP v x"..
hence "P v x" by (rule proper_implies_part)
assume antecedent: "\<forall>z. PP z x \<longrightarrow> P z y"
hence "PP v x \<longrightarrow> P v y"..
hence "P v y" using `PP v x`..
with `P v x` have "P v x \<and> P v y"..
hence "\<exists>v. P v x \<and> P v y"..
with overlap_eq have "O x y"..
show "P x y"
proof (rule ccontr)
assume "\<not> P x y"
hence "\<exists>z. P z x \<and> \<not> O z y"
by (rule strong_supplementation)
then obtain z where z: "P z x \<and> \<not> O z y"..
hence "P z x"..
moreover have "z \<noteq> x"
proof
assume "z = x"
moreover from z have "\<not> O z y"..
ultimately have "\<not> O x y" by (rule subst)
thus "False" using `O x y`..
qed
ultimately have "P z x \<and> z \<noteq> x"..
with nip_eq have "PP z x"..
from antecedent have "PP z x \<longrightarrow> P z y"..
hence "P z y" using `PP z x`..
hence "O z y" by (rule part_implies_overlap)
from z have "\<not> O z y"..
thus "False" using `O z y`..
qed
qed
text \<open> Which with antisymmetry entails the extensionality of proper parthood.\footnote{See
@{cite "simons_parts:_1987"} p. 28, @{cite "varzi_parts_1996"} p. 263 and @{cite "casati_parts_1999"}
p. 40.} \<close>
theorem proper_part_extensionality:
"(\<exists>z. PP z x \<or> PP z y) \<Longrightarrow> x = y \<longleftrightarrow> (\<forall>z. PP z x \<longleftrightarrow> PP z y)"
proof -
assume antecedent: "\<exists>z. PP z x \<or> PP z y"
show "x = y \<longleftrightarrow> (\<forall>z. PP z x \<longleftrightarrow> PP z y)"
proof
assume "x = y"
moreover have "\<forall>z. PP z x \<longleftrightarrow> PP z x" by simp
ultimately show "\<forall>z. PP z x \<longleftrightarrow> PP z y" by (rule subst)
next
assume right: "\<forall>z. PP z x \<longleftrightarrow> PP z y"
have "\<forall>z. PP z x \<longrightarrow> P z y"
proof
fix z
show "PP z x \<longrightarrow> P z y"
proof
assume "PP z x"
from right have "PP z x \<longleftrightarrow> PP z y"..
hence "PP z y" using `PP z x`..
thus "P z y" by (rule proper_implies_part)
qed
qed
have "\<forall>z. PP z y \<longrightarrow> P z x"
proof
fix z
show "PP z y \<longrightarrow> P z x"
proof
assume "PP z y"
from right have "PP z x \<longleftrightarrow> PP z y"..
hence "PP z x" using `PP z y`..
thus "P z x" by (rule proper_implies_part)
qed
qed
from antecedent obtain z where z: "PP z x \<or> PP z y"..
thus "x = y"
proof (rule disjE)
assume "PP z x"
hence "\<exists>z. PP z x"..
hence "P x y" using `\<forall>z. PP z x \<longrightarrow> P z y`
by (rule proper_parts_principle)
from right have "PP z x \<longleftrightarrow> PP z y"..
hence "PP z y" using `PP z x`..
hence "\<exists>z. PP z y"..
hence "P y x" using `\<forall>z. PP z y \<longrightarrow> P z x`
by (rule proper_parts_principle)
with `P x y` show "x = y"
by (rule part_antisymmetry)
next
assume "PP z y"
hence "\<exists>z. PP z y"..
hence "P y x" using `\<forall>z. PP z y \<longrightarrow> P z x`
by (rule proper_parts_principle)
from right have "PP z x \<longleftrightarrow> PP z y"..
hence "PP z x" using `PP z y`..
hence "\<exists>z. PP z x"..
hence "P x y" using `\<forall>z. PP z x \<longrightarrow> P z y`
by (rule proper_parts_principle)
thus "x = y"
using `P y x` by (rule part_antisymmetry)
qed
qed
qed
text \<open> It also follows from strong supplementation that parthood is definable in terms of overlap.\footnote{
See @{cite "parsons_many_2014"} p. 4.} \<close>
lemma part_overlap_eq: "P x y \<longleftrightarrow> (\<forall>z. O z x \<longrightarrow> O z y)"
proof
assume "P x y"
show "(\<forall>z. O z x \<longrightarrow> O z y)"
proof
fix z
show "O z x \<longrightarrow> O z y"
proof
assume "O z x"
with `P x y` show "O z y"
by (rule overlap_monotonicity)
qed
qed
next
assume right: "\<forall>z. O z x \<longrightarrow> O z y"
show "P x y"
proof (rule ccontr)
assume "\<not> P x y"
hence "\<exists>z. P z x \<and> \<not> O z y"
by (rule strong_supplementation)
then obtain z where z: "P z x \<and> \<not> O z y"..
hence "\<not> O z y"..
from right have "O z x \<longrightarrow> O z y"..
moreover from z have "P z x"..
hence "O z x" by (rule part_implies_overlap)
ultimately have "O z y"..
with `\<not> O z y` show "False"..
qed
qed
text \<open> Which entails the extensionality of overlap. \<close>
theorem overlap_extensionality: "x = y \<longleftrightarrow> (\<forall>z. O z x \<longleftrightarrow> O z y)"
proof
assume "x = y"
moreover have "\<forall>z. O z x \<longleftrightarrow> O z x"
proof
fix z
show "O z x \<longleftrightarrow> O z x"..
qed
ultimately show "\<forall>z. O z x \<longleftrightarrow> O z y"
by (rule subst)
next
assume right: "\<forall>z. O z x \<longleftrightarrow> O z y"
have "\<forall>z. O z y \<longrightarrow> O z x"
proof
fix z
from right have "O z x \<longleftrightarrow> O z y"..
thus "O z y \<longrightarrow> O z x"..
qed
with part_overlap_eq have "P y x"..
have "\<forall>z. O z x \<longrightarrow> O z y"
proof
fix z
from right have "O z x \<longleftrightarrow> O z y"..
thus "O z x \<longrightarrow> O z y"..
qed
with part_overlap_eq have "P x y"..
thus "x = y"
using `P y x` by (rule part_antisymmetry)
qed
end
(*<*) end (*>*)
\ No newline at end of file
This diff is collapsed.
section \<open> General Mereology \<close>
(*<*)
theory GM
imports CM
begin (*>*)
text \<open> The theory of \emph{general mereology} adds the axiom of fusion to ground mereology.\footnote{
See @{cite "simons_parts:_1987"} p. 36, @{cite "varzi_parts_1996"} p. 265 and @{cite "casati_parts_1999"} p. 46.} \<close>
locale GM = M +
assumes fusion:
"\<exists> x. \<phi> x \<Longrightarrow> \<exists> z. \<forall> y. O y z \<longleftrightarrow> (\<exists> x. \<phi> x \<and> O y x)"
begin
text \<open> Fusion entails sum closure. \<close>
theorem sum_closure: "\<exists> z. \<forall> w. O w z \<longleftrightarrow> (O w a \<or> O w b)"
proof -
have "a = a"..
hence "a = a \<or> a = b"..
hence "\<exists> x. x = a \<or> x = b"..
hence "(\<exists> z. \<forall> y. O y z \<longleftrightarrow> (\<exists> x. (x = a \<or> x = b) \<and> O y x))"
by (rule fusion)
then obtain z where z:
"\<forall> y. O y z \<longleftrightarrow> (\<exists> x. (x = a \<or> x = b) \<and> O y x)"..
have "\<forall> w. O w z \<longleftrightarrow> (O w a \<or> O w b)"
proof
fix w
from z have w: "O w z \<longleftrightarrow> (\<exists> x. (x = a \<or> x = b) \<and> O w x)"..
show "O w z \<longleftrightarrow> (O w a \<or> O w b)"
proof
assume "O w z"
with w have "\<exists> x. (x = a \<or> x = b) \<and> O w x"..
then obtain x where x: "(x = a \<or> x = b) \<and> O w x"..
hence "O w x"..
from x have "x = a \<or> x = b"..
thus "O w a \<or> O w b"
proof (rule disjE)
assume "x = a"
hence "O w a" using `O w x` by (rule subst)
thus "O w a \<or> O w b"..
next
assume "x = b"
hence "O w b" using `O w x` by (rule subst)
thus "O w a \<or> O w b"..
qed
next
assume "O w a \<or> O w b"
hence "\<exists> x. (x = a \<or> x = b) \<and> O w x"
proof (rule disjE)
assume "O w a"
with `a = a \<or> a = b` have "(a = a \<or> a = b) \<and> O w a"..
thus "\<exists> x. (x = a \<or> x = b) \<and> O w x"..
next
have "b = b"..
hence "b = a \<or> b = b"..
moreover assume "O w b"
ultimately have "(b = a \<or> b = b) \<and> O w b"..
thus "\<exists> x. (x = a \<or> x = b) \<and> O w x"..
qed
with w show "O w z"..
qed
qed
thus "\<exists> z. \<forall> w. O w z \<longleftrightarrow> (O w a \<or> O w b)"..
qed
end
(*<*) end (*>*)
section \<open> General Minimal Mereology \<close>
(*<*)
theory GMM
imports GM MM
begin
(*>*)
text \<open> The theory of \emph{general minimal mereology} adds general mereology to minimal mereology.\footnote{
See @{cite "casati_parts_1999"} p. 46.} \<close>
locale GMM = GM + MM
begin
text \<open> It is natural to assume that just as closed minimal mereology and closed extensional mereology
are the same theory, so are general minimal mereology and general extensional mereology.\footnote{For
this mistake see @{cite "simons_parts:_1987"} p. 37 and @{cite "casati_parts_1999"} p. 46. The mistake
is corrected in @{cite "pontow_note_2004"} and @{cite "hovda_what_2009"}. For discussion of the significance
of this issue see, for example, @{cite "varzi_universalism_2009"} and @{cite "cotnoir_does_2016"}.}
But this is not the case, since the proof of strong supplementation in closed minimal mereology
required the product closure axiom. However, in general minimal mereology, the fusion axiom does not
entail the product closure axiom. So neither product closure nor strong supplementation are theorems. \<close>
lemma product_closure:
"O x y \<Longrightarrow> (\<exists> z. \<forall> v. P v z \<longleftrightarrow> P v x \<and> P v y)"
nitpick [expect = genuine] oops
lemma strong_supplementation: "\<not> P x y \<Longrightarrow> (\<exists> z. P z x \<and> \<not> O z y)"
nitpick [expect = genuine] oops
end
(*<*) end (*>*)
\ No newline at end of file
section \<open> Ground Mereology \<close>
(*<*)
theory M
imports PM
begin
(*>*)
text \<open> The theory of \emph{ground mereology} adds to premereology the antisymmetry of parthood, and
defines proper parthood as nonidentical parthood.\footnote{For this axiomatization of ground mereology see,
for example, @{cite "varzi_parts_1996"} p. 261 and @{cite "casati_parts_1999"} p. 36. For discussion of the
antisymmetry of parthood see, for example, @{cite "cotnoir_antisymmetry_2010"}. For the definition of
proper parthood as nonidentical parthood, see for example, @{cite "leonard_calculus_1940"} p. 47.}
In other words, ground mereology assumes that parthood is a partial order.\<close>
locale M = PM +
assumes part_antisymmetry: "P x y \<Longrightarrow> P y x \<Longrightarrow> x = y"
assumes nip_eq: "PP x y \<longleftrightarrow> P x y \<and> x \<noteq> y"
begin
subsection \<open> Proper Parthood \<close>
lemma proper_implies_part: "PP x y \<Longrightarrow> P x y"
proof -
assume "PP x y"
with nip_eq have "P x y \<and> x \<noteq> y"..
thus "P x y"..
qed
lemma proper_implies_distinct: "PP x y \<Longrightarrow> x \<noteq> y"
proof -
assume "PP x y"
with nip_eq have "P x y \<and> x \<noteq> y"..
thus "x \<noteq> y"..
qed
lemma proper_implies_not_part: "PP x y \<Longrightarrow> \<not> P y x"
proof -
assume "PP x y"
hence "P x y" by (rule proper_implies_part)
show "\<not> P y x"
proof
from `PP x y` have "x \<noteq> y" by (rule proper_implies_distinct)
moreover assume "P y x"
with `P x y` have "x = y" by (rule part_antisymmetry)
ultimately show "False"..
qed
qed
lemma proper_part_asymmetry: "PP x y \<Longrightarrow> \<not> PP y x"
proof -
assume "PP x y"
hence "P x y" by (rule proper_implies_part)
from `PP x y` have "x \<noteq> y" by (rule proper_implies_distinct)
show "\<not> PP y x"
proof
assume "PP y x"
hence "P y x" by (rule proper_implies_part)
with `P x y` have "x = y" by (rule part_antisymmetry)
with `x \<noteq> y` show "False"..
qed
qed
lemma proper_implies_overlap: "PP x y \<Longrightarrow> O x y"
proof -
assume "PP x y"
hence "P x y" by (rule proper_implies_part)
thus "O x y" by (rule part_implies_overlap)
qed
end
text \<open> The rest of this section compares four alternative axiomatizations of ground mereology, and
verifies their equivalence. \<close>
text \<open> The first alternative axiomatization defines proper parthood as nonmutual instead of nonidentical parthood.\footnote{
See, for example, @{cite "varzi_parts_1996"} p. 261 and @{cite "casati_parts_1999"} p. 36. For the distinction
between nonmutual and nonidentical parthood, see @{cite "parsons_many_2014"} pp. 6-8.}
In the presence of antisymmetry, the two definitions of proper parthood are equivalent.\footnote{
See @{cite "cotnoir_antisymmetry_2010"} p. 398, @{cite "donnelly_using_2011"} p. 233,
@{cite "cotnoir_non-wellfounded_2012"} p. 191, @{cite "obojska_remarks_2013"} p. 344,
@{cite "cotnoir_does_2016"} p. 128 and @{cite "cotnoir_is_2018"}.} \<close>
locale M1 = PM +
assumes nmp_eq: "PP x y \<longleftrightarrow> P x y \<and> \<not> P y x"
assumes part_antisymmetry: "P x y \<Longrightarrow> P y x \<Longrightarrow> x = y"
sublocale M \<subseteq> M1
proof
fix x y
show nmp_eq: "PP x y \<longleftrightarrow> P x y \<and> \<not> P y x"
proof
assume "PP x y"
with nip_eq have nip: "P x y \<and> x \<noteq> y"..
hence "x \<noteq> y"..
from nip have "P x y"..
moreover have "\<not> P y x"
proof
assume "P y x"
with `P x y` have "x = y" by (rule part_antisymmetry)
with `x \<noteq> y` show "False"..
qed
ultimately show "P x y \<and> \<not> P y x"..
next
assume nmp: "P x y \<and> \<not> P y x"
hence "\<not> P y x"..
from nmp have "P x y"..
moreover have "x \<noteq> y"
proof
assume "x = y"
hence "\<not> P y y" using `\<not> P y x` by (rule subst)
thus "False" using part_reflexivity..
qed
ultimately have "P x y \<and> x \<noteq> y"..
with nip_eq show "PP x y"..
qed
show "P x y \<Longrightarrow> P y x \<Longrightarrow> x = y" using part_antisymmetry.
qed
sublocale M1 \<subseteq> M
proof
fix x y
show nip_eq: "PP x y \<longleftrightarrow> P x y \<and> x \<noteq> y"
proof
assume "PP x y"
with nmp_eq have nmp: "P x y \<and> \<not> P y x"..
hence "\<not> P y x"..
from nmp have "P x y"..
moreover have "x \<noteq> y"
proof
assume "x = y"
hence "\<not> P y y" using `\<not> P y x` by (rule subst)
thus "False" using part_reflexivity..
qed
ultimately show "P x y \<and> x \<noteq> y"..
next
assume nip: "P x y \<and> x \<noteq> y"
hence "x \<noteq> y"..
from nip have "P x y"..
moreover have "\<not> P y x"
proof
assume "P y x"
with `P x y` have "x = y" by (rule part_antisymmetry)
with `x \<noteq> y` show "False"..
qed
ultimately have "P x y \<and> \<not> P y x"..
with nmp_eq show "PP x y"..
qed
show "P x y \<Longrightarrow> P y x \<Longrightarrow> x = y" using part_antisymmetry.
qed
text \<open> Conversely, assuming the two definitions of proper parthood are equivalent entails the antisymmetry
of parthood, leading to the second alternative axiomatization, which assumes both equivalencies.\footnote{
For this point see especially @{cite "parsons_many_2014"} pp. 9-10.} \<close>
locale M2 = PM +
assumes nip_eq: "PP x y \<longleftrightarrow> P x y \<and> x \<noteq> y"
assumes nmp_eq: "PP x y \<longleftrightarrow> P x y \<and> \<not> P y x"
sublocale M \<subseteq> M2
proof
fix x y
show "PP x y \<longleftrightarrow> P x y \<and> x \<noteq> y" using nip_eq.
show "PP x y \<longleftrightarrow> P x y \<and> \<not> P y x" using nmp_eq.
qed
sublocale M2 \<subseteq> M
proof
fix x y
show "PP x y \<longleftrightarrow> P x y \<and> x \<noteq> y" using nip_eq.
show "P x y \<Longrightarrow> P y x \<Longrightarrow> x = y"
proof -
assume "P x y"
assume "P y x"
show "x = y"
proof (rule ccontr)
assume "x \<noteq> y"
with `P x y` have "P x y \<and> x \<noteq> y"..
with nip_eq have "PP x y"..
with nmp_eq have "P x y \<and> \<not> P y x"..
hence "\<not> P y x"..
thus "False" using `P y x`..
qed
qed
qed
text \<open> In the context of the other axioms, antisymmetry is equivalent to the extensionality of parthood,
which gives the third alternative axiomatization.\footnote{For this point see @{cite "cotnoir_antisymmetry_2010"} p. 401
and @{cite "cotnoir_non-wellfounded_2012"} p. 191-2.} \<close>
locale M3 = PM +
assumes nip_eq: "PP x y \<longleftrightarrow> P x y \<and> x \<noteq> y"
assumes part_extensionality: "x = y \<longleftrightarrow> (\<forall> z. P z x \<longleftrightarrow> P z y)"
sublocale M \<subseteq> M3
proof
fix x y
show "PP x y \<longleftrightarrow> P x y \<and> x \<noteq> y" using nip_eq.
show part_extensionality: "x = y \<longleftrightarrow> (\<forall> z. P z x \<longleftrightarrow> P z y)"
proof
assume "x = y"
moreover have "\<forall> z. P z x \<longleftrightarrow> P z x" by simp
ultimately show "\<forall> z. P z x \<longleftrightarrow> P z y" by (rule subst)
next
assume z: "\<forall> z. P z x \<longleftrightarrow> P z y"
show "x = y"
proof (rule part_antisymmetry)
from z have "P y x \<longleftrightarrow> P y y"..
moreover have "P y y" by (rule part_reflexivity)
ultimately show "P y x"..
next
from z have "P x x \<longleftrightarrow> P x y"..
moreover have "P x x" by (rule part_reflexivity)
ultimately show "P x y"..
qed
qed
qed
sublocale M3 \<subseteq> M
proof
fix x y
show "PP x y \<longleftrightarrow> P x y \<and> x \<noteq> y" using nip_eq.
show part_antisymmetry: "P x y \<Longrightarrow> P y x \<Longrightarrow> x = y"
proof -
assume "P x y"
assume "P y x"
have "\<forall> z. P z x \<longleftrightarrow> P z y"
proof
fix z
show "P z x \<longleftrightarrow> P z y"
proof
assume "P z x"
thus "P z y" using `P x y` by (rule part_transitivity)
next
assume "P z y"
thus "P z x" using `P y x` by (rule part_transitivity)
qed
qed
with part_extensionality show "x = y"..
qed
qed
text \<open>The fourth axiomatization adopts proper parthood as primitive.\footnote{See, for example,
@{cite "simons_parts:_1987"}, p. 26 and @{cite "casati_parts_1999"} p. 37.} Improper parthood is
defined as proper parthood or identity.\<close>
locale M4 =
assumes part_eq: "P x y \<longleftrightarrow> PP x y \<or> x = y"
assumes overlap_eq: "O x y \<longleftrightarrow> (\<exists> z. P z x \<and> P z y)"
assumes proper_part_asymmetry: "PP x y \<Longrightarrow> \<not> PP y x"
assumes proper_part_transitivity: "PP x y \<Longrightarrow> PP y z \<Longrightarrow> PP x z"
begin
lemma proper_part_irreflexivity: "\<not> PP x x"
proof
assume "PP x x"
hence "\<not> PP x x" by (rule proper_part_asymmetry)
thus "False" using `PP x x`..
qed
end
sublocale M \<subseteq> M4
proof
fix x y z
show part_eq: "P x y \<longleftrightarrow> (PP x y \<or> x = y)"
proof
assume "P x y"
show "PP x y \<or> x = y"
proof cases
assume "x = y"
thus "PP x y \<or> x = y"..
next
assume "x \<noteq> y"
with `P x y` have "P x y \<and> x \<noteq> y"..
with nip_eq have "PP x y"..
thus "PP x y \<or> x = y"..
qed
next
assume "PP x y \<or> x = y"
thus "P x y"
proof
assume "PP x y"
thus "P x y" by (rule proper_implies_part)
next
assume "x = y"
thus "P x y" by (rule identity_implies_part)
qed
qed
show "O x y \<longleftrightarrow> (\<exists> z. P z x \<and> P z y)" using overlap_eq.
show "PP x y \<Longrightarrow> \<not> PP y x" using proper_part_asymmetry.
show proper_part_transitivity: "PP x y \<Longrightarrow> PP y z \<Longrightarrow> PP x z"
proof -
assume "PP x y"
assume "PP y z"
have "P x z \<and> x \<noteq> z"
proof
from `PP x y` have "P x y" by (rule proper_implies_part)
moreover from `PP y z` have "P y z" by (rule proper_implies_part)
ultimately show "P x z" by (rule part_transitivity)
next
show "x \<noteq> z"
proof
assume "x = z"
hence "PP y x" using `PP y z` by (rule ssubst)
hence "\<not> PP x y" by (rule proper_part_asymmetry)
thus "False" using `PP x y`..
qed
qed