A "set" containing objects of diffrent types in higher order logic

Question

In higher order logic, we can model a set as a function whose images lie in the type of propositions. For example, the singleton $\{0\}$ can be modeled as the function $f: <type\ of\ 0> \rightarrow Prop$ such that $f(x) = True \iff x = 0$

But this way to do doesn't permit to create a set whose elements have different types. For example, the set containing only $0$ and $\{0\}$ can't be modeled as a function $f: T \rightarrow Prop$ because no type $T$ suits.

My question is: is there a way in higher order logic to model sets which permits to build sets containing elements of different types ?

The type theory I use is simply typed lambda calculus (see its Wikipedia webpage, in which the basis types of $B$ are the sort of propositions and the sort of objects)

Answer 1

One simple way is to use sum types to allow other types: for example, for types $S$ and $T$, we may consider $S+T\to\mathsf{Prop}$. If you need more types, we may sum all types of a universe type.

However, your example apparently also asks how to model iterative sets, like $\{\varnothing\}$, $\{\{\varnothing\}\}$, etc. We can emulate it by taking Aczel's type-theoretic interpretation of sets.

The main idea of Aczel's interpretation is observing a set as a (well-founded) rooted tree under $\in$: for example, we may view

• $\varnothing$ as an empty tree,
• $\{\varnothing\}$ as a tree with a node, labeled as $\varnothing$, and
• $\{\varnothing,\{\varnothing\}\}$ as a tree that comprises the root, two immediate successors of the root corresponding to $\varnothing$ and $\{\varnothing\}$, and an additional node that is an immediate successor of $\{\varnothing\}$.

Definition. Let $U$ be a universe type. Now consider the type $V$ of iterative sets that is given by the following introduction rules: $$\frac{a:U\qquad f:a\to V}{\sup(a,f):V}$$

For every $\alpha\equiv \sup(a,f)$, we write $\overline{\alpha}=a$ and $\tilde{\alpha}=f$.

We also need to define the equality and the membership relation $\in$ over $V$. Note that the 'equality' over $V$ is not the same as the propositional equality.

Definition. Let $\alpha,\beta:V$. Define $\alpha\mathrel{\dot{=}}\beta$ and $\alpha\mathrel{\dot{\in}}\beta$ as follows:

$$\alpha\mathrel{\dot{=}}\beta :\equiv \left(\prod_{x:\overline{\alpha}}\sum_{y:\overline{\beta}} \tilde{\alpha}(x)\mathrel{\dot{=}}\tilde{\beta}(y)\right)\times \left(\prod_{x:\overline{\beta}}\sum_{y:\overline{\alpha}} \tilde{\alpha}(x)\mathrel{\dot{=}}\tilde{\beta}(y)\right),$$ $$\alpha\mathrel{\dot{\in}}\beta:\equiv \sum_{x:\overline{\beta}}(\alpha\mathrel{\dot{=}} \tilde{\beta}(x)).$$

The definition of $a\mathrel{\dot{=}}b$ and $a\mathrel{\dot{\in}}b$ ensures $V$ is extensional under $\mathrel{\dot{\in}}$. By interpreting first-order logic into type theory (especially, interpreting $\forall$ and $\exists$ using the product and sum types,) we can see that our $V$ 'satisfies' some moderate set theory known as constructive set theory $\mathsf{CZF}$. Also, if our type theory has the law of excluded middle, our interpretation will interpret the full $\mathsf{ZF}$.

As far as I know, the main idea of the interpretation (viewing sets as trees) is adopted by some proof assistants. For example, the ZFC module in Coq and Lean uses this interpretation to produce sets. (Isabelle takes a more layman-like approach, by interpreting the first-order logic and list the axioms of $\mathsf{ZFC}$.)