Mereology
Mereology (WP, nLab) is the study of parts and wholes. It is closely related to set theory, in the sense that subsets are parts of whole supersets, but is studied independently.
Axioms
We present System M, the simplest possible collection of mereological axioms. System M asserts that parthood is reflexive, antisymmetric, and transitive: a partial order. We augment System M with two additional axioms, the Axioms of Top and Bottom, which assert that the universal and null objects exist.
| Name | Statement |
|---|---|
| ax-pagbu-refl | ko'a pagbu ko'a |
| ax-pagbu-antisym | ganai ge ko'a pagbu ko'e gi ko'e pagbu ko'a gi ko'a du ko'e |
| ax-pagbu-trans | ganai ge ko'a pagbu ko'e gi ko'e pagbu ko'i gi ko'a pagbu ko'i |
| ax-pagbu-top | su'o da zo'u ko'a pagbu da |
| ax-pagbu-bot | su'o da zo'u da pagbu ko'a |
Note that {pagbu} is a primitive symbol and cannot be defined as an
extension of the basis. However, given {pagbu}, we can extend the resulting
basis with a few more definitions:
| Name | Statement |
|---|---|
| df-jompau | go ko'a jompau ko'e gi su'o da zo'u da pagbu ko'a .e ko'e |
| df-kuzypau | go ko'a kuzypau ko'e gi su'o da zo'u ko'a .e ko'e pagbu da |
Bridge to Set Theory
While it is not currently part of the database, set theory can be seen as a special case of mereology:
ganai da gripau de gi da pagbu de
This axiom is only absent because no use case has been found for it so far. This parallels the development of set theory as a finer-grained and more powerful mereology which is able to not only distinguish parthood but also elementhood.