mereology
定義
$ x<y\iff xが$ yの部分である (part, prathood)
$ x=y\coloneqq x<y\land y<x。反對稱律 (equality) $ x>y\coloneqq\neg(x<y)。$ xは$ yの部分でない
$ x<<y\coloneqq x<y\land\neg(y<x)。$ xは$ yの眞部分 (proper part)
$ x<>y\coloneqq\exist z(z<x\land z<y)。$ xと$ yは兩立する。被覆 (overlap)
$ Uxy\coloneqq\exist z(x<z\land y<z)。underlap
$ x><y\coloneqq\neg(x<>y)。$ xと$ yは互ひに素 (disjoint)
$ \sigma x\varphi(x)\coloneqq\iota x\forall y(x<>y\iff\exist z(\varphi(y)\land y<>z))。一般和 (general sum)
$ \because\iotais the define descripter
$ \pi x\varphi(x)\coloneqq\iota z\forall w(w<z\iff \forall x(\varphi(w)\to w<x))。一般積 (general product)
$ \pi x\varphi=\sigma x\forall y(\varphi(x)\to x<y).
$ x+y\coloneqq\sigma z(z<x\lor z<y)。和 (sum)
$ x+y=\iota z\forall w(w<>z\iff w<>x\lor w<>y).
$ x+y=\pi z(x<z\land y<z).
$ x\times y\coloneqq\sigma z(z<x\land z<y)。積 (product)
$ x\times y=\iota z\forall w(w<z\iff w<x\land w<y).
$ x\times y=\pi z(x<z\lor y<z).
$ \tilde x\coloneqq\sigma z(z><x)。補元 (complement)
$ \tilde x=\iota z\forall w(w<z\iff w><x).
$ x-y\coloneqq\sigma z(z<x\land z><y)。差 (difference)
$ x-y\iff \iota z\forall w(w<z\iff w<x\land w><y).
$ U\coloneqq\sigma x(x=x)。宇宙 (universe)
$ U=\pi x(x><x).