Container Theory
[see this posting to Mathoverflow]
Language: First order logic
Primitives: =, P, C read as "is equal to", "is a part of", "is contained in"
Axioms: those of first order identity theory +
Mereology:
Axioms about part-hood stem from the naive contemplation of part-hood, they are:
M1) A part of a part of an object is a part of that object
Formally this is: x P y ^ y P z -> x P z
M2) If X is not a part of Y, then there exists a part k of X such that k is disjoint of Y (i.e., k and Y have no common part).
M3) If X is part of Y and Y is a part of X, then X is identical to Y.
M4) For any property Q that holds of at least one object, there exists an object X that is a sum of all objects satisfying Q, i.e. every object satisfying Q is a part of X, and every object Y that have every object satisfying Q as a part of would have X as a part of it.
Define (atom): atom(x) <-> ~Exist y (y P x ^ ~y=x)
i.e. an atom is an object that doesn't have a proper parts.
M5) All objects are sums of atoms: for all X exists y (y is an atom ^ y P X)
From these axioms on can prove that X P X [see below], and also one can prove the following atomic comprehension schema
For any property Q that holds of at least one atom there is a sum of all atoms satisfying Q.
formally this is:
((Exists x: x is an atom ^ Q(x)) -> Exist K for every atom y [y P K <-> Q(y)])
is an axiom.
Axioms for Containment:
Define: x is a container <-> x is an atom.
C1: Power: for every container X there exists a container that contains all subcontainers of X.
where Y is a subcontainer of X iff the container X contains all of what the container Y contains.
C2: Separation: if phi is a property then for every container X there is a container Y that contains exactly all objects contained in X that satisfy phi.
C3: Collection: if phi(x,y) is a formula in which x,y occur free, and only free, then for every container A there exists a container B such that for every object x in A for which there exists an object y such that phi(x,y), then there exists an object z in B such that phi(x,z).
C4: Union: for every container A, there exists a container that containers all of what containers contained in A contains.
C5: Infinity: there exists a container that contains an empty container that is closed under singleton containment [i.e. the singleton container of a container contained in it, is also contained in it].
/ Theory definition finished.
The intuitive picture behind containers is for them to be imagined as CLOSED PARTITIONS ON SPACE, i.e. they split the totality of what is other than them into two disjoint non contacting compartments [here I didn't add contact as a primitive but if we are to grasp that fully then we'll need to add it, and by then we'll need to stipulate axioms for Mereo-topology, it can be done in a full formal manner] much as the effect of a circle, square, triangle, etc... on an Euclidean PLANE, and of a sphere, cube, pyramid,etc.. on a three -dimensional plane, etc...
Containers in this theory are stipulated to be Mereological atoms, in order to dismiss details about their parts, since we are not concerned with that, we are only concerned in their existence and their containment function.
Now containment i.e. x is contained in y is to be imagined as: there is a moment of time where y is a container and x is an atom that occurs inside y, i.e. in the spatial compartment closed by y, so if x is a container then x will partition the compartment of space inside y into two disjoint non contacting compartments.
There are no size constrains of a container to be inside another container, so here we imagine a container to be able to squeeze itself inside another container, so it can change its size over time.
Now the sum of containers, or more appropriately speaking the "extensions" made up of containers here are constructed FREELY without any constrain, the only simple constrain is for a property P to hold of at least one container, so if that is the case then we can have an aggregate of ALL containers satisfying P.
The containers of this theory do interpret Sets of ZFC, and the aggregate of containers would interpret classes over ZFC.
There are two distinct memberships that can be define in this theory One between containers, which is the one defined above, and the other is between a container and the aggregate of containers it is a part of, so we have
x is an 'element' of y <-> y is aggregate of containers ^ x is a container ^ x P y.
This theory can accommodate any non-well founded relation, also can formalize all sorts of Ur-elements, and can speak of any kind of classes, proper classes or not. It also can explain paradoxes and render them non-paradoxical! (intuitively speaking).
Also for beginners who need to avoid having intuitions that might lead them to paradoxes in set\class theory, this theory is very easy to handle, and therefore its very SAFE.
The proof of X P X is: for a proof by negation suppose that ~ X P X, then by M2 there must exist a part k of X such that k is disjoint of X, but whatever part of k is a part of X (M1), so k must not have any part of it, now take the question about k P k either this is true which contradict k having no parts, or k is not a part of k but by then M2 would lead to existence of a part L of k that is disjoint of k, which is a contradiction since k has no parts! QED
Another version that is equivalent to ZF-Regularity:
The Latex version:
**Intuitive background:** Objects of this theory are totalities of mereological atoms (indivisible objects), for simplicity they can be depicted as linear aggregates of atoms $\bullet \bullet \bullet \dots \bullet$, so in mereological terms they are fusions of atoms. Now $x \bullet y$ means that $y$ is a totality (aggregate/heap/conglomerate) of atoms and $x$ is one of the atoms of $y$. On the other hand "containers" are like vessels, i.e. objects enclosing some space, and the containment relation is the relation that a container bears to a container containing it, hence the symbol $\circledcirc$, so $x \circledcirc y$ to be viewed as $x$ being the inner circle, and $y$ the outer one, denoting that $x$ is a container contained by $y$, i.e. lies in a space enclosed by container $y$ at some moment of time. Clearly the symbol "${\raise{0.5 pt}\bigcirc}$" would denote an empty container, where at no moment of time a container is contained by it. It is still a container, because it encloses space! Now, because this theory is meant with aggregates of containers, therefore proper parts of containers are immaterial and so all containers are treated as mereological atoms, i.e. have no proper parts. Also, because we don't desire objects other than aggregates of containers, then all mereological atoms are stipulated to be containers which could be empty or not.
**Language:** mono-sorted first order logic with equality, extended with primitive binary relations of "$\bullet$" standing for "is an atom part of", and "$\circledcirc$" standing for "is contained in".
**Axioms:**
**Atomhood:** $y \bullet x \to \forall z \, ( z \bullet y \leftrightarrow z = y)$
**Extensionality:** $\forall z \, (z \bullet x \leftrightarrow z \bullet y ) \to x=y$
**Atomicity:** $\forall x \exists y: y \bullet x$
***Define:*** $(x = {\large \int} z: \varphi) \iff \forall y \, ( y \bullet x \leftrightarrow \exists z: \varphi(z) \land y \bullet z)$
"${\large \int} z: \varphi$" is read as the sum (aka: fusion) of all $z$ realizing $\varphi$, which is the totality of all atoms of objects realizing $\varphi$.
**Purity:** $x \bullet x \leftrightarrow \exists y\, (y \circledcirc x) \lor \exists y \, (x \circledcirc y)$
**Uniqueness:** $\forall z \, (z \circledcirc x \leftrightarrow z \circledcirc y) \to x=y$
**Empty:** $\exists x \forall y : \neg y \circledcirc x$
***Define:*** $x=\{y \mid \varphi\} \iff \forall y \, (y \circledcirc x \leftrightarrow \varphi )$
***Define:*** ${\raise{0.5 pt}\bigcirc} = \{y \mid y \neq y\}$
**Parallelism:** $\exists a \exists b \, \varphi(a,b) \land \forall a \forall b (\varphi(a,b) \to a \bullet a) \land \varphi \text { is 1:1} \to \\ (\exists x=\{a \mid \exists b \, \varphi(a,b)\} \leftrightarrow \exists x= {\large \int} b : \exists a \, \varphi(a,b) ) $
***Define:*** $x=\{a\} \iff a \bullet a \land x=\{y | y=a\}$
**Infinity:** $\exists x: {\raise{0.5 pt}\bigcirc} \bullet x \land \forall y \, (y \bullet x \to \{y\} \bullet x) $
Note: the formula $\varphi$ in parallelism must not have the symbol "$x$" occurring free. $\text {1:1}$ signify description of a one-to-one relation.
Here we can define "set" simply as an atom, so:
$\operatorname {set}(x) \iff x \bullet x$
, but more meaningfully, albeit equivalently, as:
$\operatorname{set}(x) \iff \exists y \, (y \circledcirc x) \lor x = \raise{0.5pt}\bigcirc$
$\sf ZF-Reg.$ would be easily interpreted if we take the domain formula to be "$\operatorname {set}(\cdot)$", and $\circledcirc$ to be the set-membership relation.
So, sets are containers, and membership $\in$ is the relation $\circledcirc$, which is containment of containers by containers; more explicitly, the temporary occurrence of a container within a compartment of space enclosed by a container.
The above system can be interpreted in $\sf ZF-Reg.$ by defining a preatom as a singleton of a set of singleton or empty sets; then defining a relation $\in^*$ that sends the elements of the elements of a preatom to that preatom. Formally:
$\operatorname {preatom} (x) \iff \exists y: \forall z \in y \, (\operatorname {singleton}(z) \lor z = \emptyset) \land x=\{y\}$
$y \in^* x \iff \operatorname {preatom}(x) \land y \in \bigcup x$
Now, we define "atom" as a set that is $\in^*$-hereditarily preatom. That is:
$y \in^*_0 x \iff y \in^* x \\ y \in^*_{n+1} x \iff \exists z \, (z \in^*_n x \land y \in^* z) \\ \operatorname {atom}(x) \iff \operatorname {preatom}(x) \land \forall n \in \omega: \forall y (y \in^*_n x \to \operatorname {preatom}(y))$
Now we limit the domain to set unions of nonempty sets of atoms, then define $\bullet$ and $\circledcirc$ as:
$y \bullet x \iff y \subseteq x \land \operatorname {singleton}(y) $
$y \circledcirc x \iff y \in^* x $
This way we get to interpret all the above system in $\sf ZF-Reg.$.
The normal version
Intuitive background: Objects of this theory are totalities of mereological atoms (indivisible objects), for simplicity they can be depicted as linear aggregates of atoms .... . . ., so in mereological terms they are fusions of atoms. Now x.y means that y is a totality (aggregate/heap/conglomerate) of atoms and x is one of the atoms of y . On the other hand "containers" are like vessels, i.e. objects enclosing some space, and the containment relation is the relation that a container bears to a container containing it, hence the symbol ⊚ , so x⊚y to be viewed as x being the inner circle, and y the outer one, denoting that x is a container contained by y , i.e. lies in a space enclosed by container y at some moment of time. Clearly the symbol "◯" would denote an empty container, where at no moment of time a container is contained by it. It is still a container, because it encloses space! Now, because this theory is meant with aggregates of containers, therefore proper parts of containers are immaterial and so all containers are treated as mereological atoms, i.e. have no proper parts. Also, because we don't desire objects other than aggregates of containers, then all mereological atoms are stipulated to be containers which could be empty or not.
Language: mono-sorted first order logic with equality, extended with primitive binary relations of "." standing for "is an atom part of", and "⊚" standing for "is contained in".
Axioms:
Atomhood: y.x → ∀z (z.y ↔ z=y)
Extensionality: ∀z (z.x ↔ z.y) → x=y
Atomicity: ∀x∃y: y.x
Define: (x= ∫z: φ) ⟺ ∀y (y.x ↔ ∃z: φ(z) ∧ y.z)
"∫z: φ" is read as the sum (aka: fusion) of all z realizing φ, which is the totality of all atoms of objects realizing φ.
Purity: x.x ↔ ∃y (y⊚x) ∨ ∃y (x⊚y)
Uniqueness: ∀z (z⊚x ↔ z⊚y) → x=y
Empty: ∃x∀y: ¬ y⊚x
Define: x = {y∣φ} ⟺ ∀y (y⊚x ↔ ∃z: φ(z) ∧ y.z)
Define: ◯ = {y∣ y≠y}
Parallelism: ∃a∃b φ(a,b) ∧ ∀a∀b (φ(a,b)→a.a) ∧ φ is 1:1→
( ∃x={a∣ ∃b φ(a,b)} ↔ ∃x=∫b:∃a φ(a,b) )
Define: x={a} ⟺ a.a ∧ x={y|y=a}
Infinity: ∃x : ◯.x ∧ ∀y (y.x → {y}∙x)
Note: the formula φ in parallelism must not have the symbol "x" occurring free. 1:1 signify description of a one-to-one relation.
Here we can define "set" simply as an atom, so:
set(x)⟺x.x
, but more meaningfully, albeit equivalently, as:
set(x) ⟺ ∃y (y⊚x) ∨ x=◯
ZF−Reg. would be easily interpreted if we take the domain formula to be "set(⋅)
", and ⊚ to be the set-membership relation.
So, sets are containers, and membership ∈ is the relation ⊚, which is containment of containers by containers; more explicitly, the temporary occurrence of a container within a compartment of space enclosed by a container.
The above system can be interpreted in ZF−Reg. by defining "preatom" as a singleton of a set of singleton or empty sets; then defining relation ∈∗ that sends the elements of the elements of a preatom to that preatom. Formally:
preatom(x) ⟺ ∃y: ∀z∈y (singleton(z) ∨ z=∅) ∧ x={y}
y∈∗x ⟺ preatom(x) ∧ y∈⋃x
Now, we define "atom" as a set that is ∈∗-hereditarily preatom. That is:
y ∈∗0 x ⟺ y ∈∗ x
y ∈∗n+1 x ⟺ ∃z (z ∈∗n x ∧ y ∈∗ z)
atom(x) ⟺ preatom(x) ∧ ∀n∈ω: ∀y (y ∈∗n x → preatom(y))
Now we limit the domain to set unions of nonempty sets of atoms, then define . and ⊚ as:
y.x ⟺ y⊆x ∧ singleton(y)
y⊚x ⟺ y∈∗x
This way we get to interpret all the above system in ZF−Reg..
Since this theory is an admix of Mereology and Containment, then I'd call it as Mereological Container Theory "MCT".
See: mathoverflow.net/q/464282/95347
See also the pdf file uploaded by the end of this page.
This theory easily extends to Morse-Kelley set theory, since the general sum principle (Atomic unrestricted composition) is already a known principle of Atomic General Extensional Mereology. But, this requires some minor modifications, so we need to tweak Parallelism and Infinity in the following manner:
Parallelism: ∃pieces a,b φ(a,b) ∧ φ is 1:1 →[∃x = {a∣∃b φ(a,b)} ↔ ∃x = ∫b: piece(b) ∧ ∃a φ(a,b)]
Infinity: ∃x: ◯⊚x ∧ ∀y (y⊚x → {y}⊚x)
Of course we need to add the general sum principle which is simply:
Composition: ∃yφ →∃x:x = ∫y: φ
Of course x must not occur free in φ.
Now a piece is defined as a part of a containment complex, the latter is the fusion of a container and its contents.
Define: piece(x)⟺∃a: a.a ∧ ∀y (y.x → y=a ∨ y⊚a)
Other versions interpreting other theoreis:
I think it might be possible to find some NATURAL explanation to NF in terms of mereo-container set theory. A theory that parallels containers after pure extensions.
We take "atomic part-hood" to be our primitive, denote it by small p, so 'x p y' is read as "x is an atom that is a part of y", now we lay down axioms about it:
1. Atomicity: \forall x \exists y (y p x)
2. Atoms: \forall x,y (x p y \to \forall z (z p x \to z=x))
define: atom(x) \iff \exists y (x p y)
3. Extensionality: \forall x,y (\forall z (z p x \iff z p y) \to x=y)
4. Comprehension schema: if phi(y) is a formula in which x is not free, then
\exists an atom y (phi(y)) \to \exists x \forall y (y p x \iff atom(y) phi), is an axiom.
we define this extension as: x= [y|phi]
Add the primitive C, denoting the relation "is contained in" [imagined trivially as
vessels into which things can be put]
Define: x={y|phi} <-> \forall y (y C x <-> phi)
5. Axiom schema of Paralleling: if by phi^C it is meant a formula obtained from the formula phi which only use =,p as predicates [i.e. phi is a pure extensional formula], by merely replacing all occurrences of p in phi by C. [where x do not occur in phi) then:
\exists atom y (phi(y)) ^ \exists atom y (~phi(y)) \to
\exists x (x={y|phi^C})
is an axiom.
Define (container): \forall x (container(x) <-> atom(x))
6. Empty set: \exists a container x [\neg \exists y (y C x)]
I think this might interpret NF, notice that if we remove the second condition in the antecedent, then we may get something like positive set theory.
Older version:
Informal understanding of Aggregate-Container theory. Aggregates are taken to be wholes of atoms in the Mereological sense. For simplicity all objects are taken to be fusions of atoms, in other words for every object x every object y that overlaps (have a shared part) with x would overlap with an atom that is a part of x. Atomic supplementation states that if x is not a part of y then there must be an atom that is a part of x that is not a part of y. Now the *unrestricted Atomic Sum principle* would allow formation of any collection of atoms satisfying a formula phi once there is at least one atom that satisfies phi. Of course an atom is an object that has itself as the only part. The primitive relation part partially orders the universe. bottom object doesn't exist, so there is no object that is a part of every object. Now all of that is usual Atomic Mereology. Now the relation that an atom bears to the aggregate it is a part of, is what we call as 'aggregate-membership' relation. What's new in this theory is its informal vision about 'containers' which are taken to paraphrase 'sets' as present in set theory. Containers can be informally understood as closed boundaries, like a line that encircles an aggregate of objects. Now a container divides space into two main compartments: inside the container and what is not inside the container. Now the aggregate of all objects inside the container is said to be 'contained' in that container, so is every part of that aggregate. This is like for example three specific eggs in some specific basket, the basket is the container and the totality (i.e. aggregate) of the three eggs is said to be 'contained' in the basket, also every aggregate of two of those eggs is also said to be 'contained' in that basket, and similarly every single egg of those is also said to be 'contained' in the basket. Now the relation that a single egg has to the basket is an example of 'set-membership' relation. More generally the relation that an 'atom' of an aggregate contained in a container bears to that container is what is named here as 'set-membership' relation. Now every object that contains an aggregate is a CONTAINER, but yet there is a CONTAINER that do not contain any aggregate inside it! that is the empty container. The general philosophy here is that those containers try as much as possible to mimic properties of aggregates, although the copying is not exact and it does break down here and there yet it is a kind of paralleling of what occurs at the aggregate level. This is found both in Extensionality of containers which is nothing but copying of Extensionality of aggregates, and also in Comprehension over containment which copies comprehension over aggregates. So a pure formula from the aggregate world (i.e. that do not mention containers and containment) after which there exists an aggregate of atoms satisfying it, would be a formula that decides containment in a container after a copied formula, this copying is done by replacing each occurrence of 'aggregate-membership' symbol in that formula by the symbol given to 'set-membership' and then we stipulate that a container exists containing objects that satisfy that copied formula. A clear mimicking principle! So 'sets' are viewed as: Containers that mimic aggregates! It is essential for this method to spell out conditions when a container becomes an atom, and this is stipulated to be when a container only contains containers inside it, a more harsh restriction is only when a container contains hereditarily 'atom container' containers inside it. At last it is more aesthetic to stipulate that distinct containers are non overlapping (i.e. disjoint, aka. discrete). This method can define the set of all sets (the container of all atom containers), also can define the set of all self membered sets, the set of all singletons that are self membered, etc.... something that NF cannot. So it speaks about some large sets that NF cannot address! This method is quite strong compared to NFU, it does interpret FULL second order arithmetic by working on aggregates of hereditarily atom container containers. It is nice to see how the customary well known set theoretic paradoxes are avoided in this theory! it is a nice piece of knowledge and is trivial to speak about it. Formal Exposition: Name: Aggregate-Container Theory Language: FOL Primitives: P for 'is part of'; Monadic C for "is a container"; Dyadic C for "is contained in". Axioms: [1] x P y P z -> x P z [2] x P x Def.): x=y <-> x P y & y P x Def.): atom(x)<-> Ay. y P x -> x P y Def.): x e y <-> x P y & atom(x) [3] Ax(Ey e x) [4] Az(z e y -> z e x) -> y P x [5] Ey(atom(y)phi) ->ExAy(y e x <-> atom(y)phi) Def.): k=[x|phi] <-> Ax(x e k <-> phi) [6] y C x -> C(x) [7] y C x & z P y -> z C x Def.): y E x <-> Ez(z C x & y e z) [8] C(x) & C(y) ->(Az(z E x <-> z E y) -> x=y) [9] Ex. C(x) & ~Ey. y C x Def.): k={x|phi} <-> Ax(x E k <-> phi) [10] [x|phi] exists -> {x|phi*} exists. where phi do not have C occurring in it, and phi* is obtained from phi by replacing each occurrence of e by C (dyadic). [11] (Ay. y E x -> C(y)) -> atom(x) [12] C(x) & C(y) & Ez(z P x & z P y) ->x=y /Theory definition finished. A nice observation is to see that if we replace 10 and 11 by the following axioms: [10] [a,b]exists ->{a,b} exists. [11] C(x) -> atom(x) then this is quite enough to interpret second order arithemtic in which most of ordinary mathematics is formalizable. A pure class\set varient of this observation is the theory in first order logic with identity, with e as the only extra-logical symbol, with the following axioms: [1] if phi is a formula in which x is not free, then (E!xAy(y e x <-> Ek(y e k) & phi)) is an axiom. [2] Ay(y e x ->y=a or y=b) ->Ek(x e k). Actually the pairing axiom can be further restricted to be only of empty or singleton classes (or containers). So we can have: [10] a,b are singleton or empty containers -> {a,b}exists. [2] (a,b are singleton or empty classes & Ay(y e x ->y=a or y=b)) -> Ek(x e k) This is 'semi-constructive' since it is imaginable to construct an encircling object around a pair of containers that are built by successive finite singlton encirclings (hereditarily singleton or empty containers) starting form the empty container. The first 9 axioms have clear justification even on constructive grounds, so the result is that second order arithmetic have strong justification for it being consistent, almost semi-constructive justification. The main merit of the 12 axiom system outlined above is that it can address some big sets that are not definable in NF, like the set of all self membered sets, the set of all singletons that are members of their elements, the set of all sets that are members of members of there elements etc.... So it might assisst in understanding such constructions.
Late note: the latest two container theories that use the paralleling principle are inconsistent.
Zuhair Al-Johar 8/11/2013