Omega-Sets

Idea

In realizability, an $\omega$-set is a set whose elements are equipped with computational evidence, or realisers. It may be regarded as a realised set, rather than merely a bare set: an element $x:X$ is accompanied by natural numbers witnessing or representing it.

The category of $\omega$-sets is also commonly called the category of assemblies. Predicates and propositions can be modelled using such realized data, but an $\omega$-set may represent arbitrary data types, not only propositions.

A modest set is an $\omega$-set in which a realiser determines at most one element.

Definition

An $\omega$-set is a set $X$ equipped with an existence predicate

$$⊩:\mathbb{N}\to X\to \mathrm{Prop}$$

that is left-total.

Equivalently, each element $x:X$ is assigned an inhabited set of natural-number realisers

$$E(x)\subseteq \mathbb{N}.$$

There is no requirement that distinct elements have disjoint sets of realisers. Thus it may be possible for

$$n\in E(x)\cap E(y)$$

even when

$$x\ne y.$$

A morphism of $\omega$-sets

$$f:(X,E_X)\to (Y,E_Y)$$

is a function $f:X\to Y$ tracked by a partial recursive function: there is some code $e\in \mathbb{N}$ such that, whenever $n\in E_X(x)$,

$$e\cdot n\downarrow \text{and}e\cdot n\in E_Y(f(x)).$$

Modest sets

A modest set is an $\omega$-set satisfying

$$E(x)\cap E(y)\ne \varnothing ⟹x=y.$$

Thus each natural-number realiser identifies at most one element. Modest sets are equivalent to partial equivalence relations on $\mathbb{N}$.

References

¹²

Footnotes

1. hyland1988-omega-sets does not define $\omega$-sets under that name. It defines modest sets, which are equivalently $\omega$-sets satisfying the additional disjointness condition on realisers.

2. jacobs1999-categorical-logic, §1.2.