# How to formalize unary intersection operator?

How can we formalize the $$\cap$$ (unary intersection) operator? Following is my attempt.

I define/construct the function $$~\cap : P(P(U)) \to P(U)$$ such that:

$$\forall a\in P(P(U)): \forall b\in U: [b\in \cap a \iff \forall c\in a:b\in c]$$

where $$U$$ is the underlying set being considered, and $$P$$ is the powerset operator. $$P(P(U))$$ can be thought of as the set of all families of subsets of $$U$$.

More work is required, but, using a formal set theory loosely based on ZFC, I have proven that $$\cap \emptyset = U$$.

Am I on the right track?

• It looks OK. Is there anything in particular about your formalisation that you are unsure about? Commented Jun 14 at 19:36
• @RobArthan I still need to establish some other fundamental results. Can you suggest any? Is this a novel approach? Commented Jun 14 at 19:58
• What you are doing is just the standard way of specifying the usual set theory operators relative to a given universal set $U$ in terms of the membership relation. Commented Jun 14 at 20:05
• @RobArthan Good to know it is a fairly standard approach, but I wouldn't call it a "universal set." (See Russell's Paradox.) I meant it to be an arbitrary set, as big or as small as you want. Think of it as similar to the underlying set in group theory. Commented Jun 14 at 20:19
• It is a universal set in the sense that, because you wish to assign meaning to $\bigcap \emptyset$, you need to restrict attention to subsets of some given container set. This is a universe in the sense of model theory and universal algebra: it is the universe of discourse in some domain of interest. Unfortunately, the word "universe" is used in several different senses in the literature. Commented Jun 14 at 20:24

For non-empty families $$X$$ and $$Y$$ of subsets of $$U$$, I was able to prove:
$$~~~~~~(\cap X)\cap (\cap Y) = \cap (X \cup Y)$$