Vepar Set Theory

The set theory in Vepar builds ZF set theory through axioms and definitions on top of Vepar HOL.

It defines operations on the $\textsf{set}$ type of Vepar HOL, including the notion of function definition and function application.

We believe that the development follows standard set theoretic definitions used by math practitioners, see e.g. Sets and relations.

If we do not say explicitly, we understand that the defined notions and their parameters are all sets, that is, have the type $\textsf{set}$ .

Pairs and Cartesian Product

$(a,b)$ is a shorthand for $\{\{ a \}, \{ a, b \} \}$ , the standard definition of an ordered pair.

$A \times B$ is $\{ (a, b)~.~a \in A \land b \in B \}$

Def: $r$ is a relation on $A,B$ if $r \subseteq A \times B$ .

Def: $f$ is a total function on $A,B$ , denoted $f:A \to B$ iff $f \subseteq A \times B$ and

$\begin{equation*} \forall x \in A. \exists^1 y. (x,y) \in f \end{equation*}$

$\begin{equation*} f@x = (\varepsilon y. (x,y) \in f) \end{equation*}$

Lemma:

$\begin{equation*} \forall A.\forall B. \forall x\in A.\forall y\in B.\forall f \colon A \to B.\ ((x,y) \in f \leftrightarrow f@x=y) \end{equation*}$

(compare to the definition in Isabelle/ZF)

$\begin{equation*} (x \in A) \mapsto t(x) \end{equation*}$

means

$\begin{equation*} \{(x,t(x)).\ x \in A \} \end{equation*}$

Lemma: For every expression $t(x)$

$\begin{equation*} \forall A. \exists B. ((x \in A) \mapsto t(x)) : A \to B \end{equation*}$