## Sunday, December 1, 2019

### Mathematics in the SOFiA language (in progress)

SOFiA is a symbolic system for writing mathematics.

The following theorem is a generalization of Russell's Paradox. To get the latter, take $\alpha$ to be a false statement and $\beta(x,y)$ to be $x\in y$. Notation: colon stands for implication and comma for conjuncton; double colon is equivalence; assumed variable is universally quantified, while conjuncted variable is existentially quantified. Note: the theorem itself is given in the last line. What precedes it is a proof.


Axioms of set theory follow. The first one is the definition of the subset relation.

$\begin{array}{l} \textbf{Def (subset).} \\ u,x,y\\\hline [x\subseteq_u y]=[z,z\in_u x:z\in_u y] \end{array}$

$\begin{array}{l} \textbf{Def (set equality). }\\ u:\mathsf{setequality}[u]=\\ x,y,x\in u,y\in u:\\\hline x=y::x\subseteq_u y,y\subseteq_u x \end{array}$

$\begin{array}{l} \textbf{Def (comprehension). }\\ u:\mathsf{comprehension}[u,\alpha,\beta]=\\ \{\beta\mid \alpha\},\{\beta\mid \alpha\}\in u,[y,y\in u:[y\in_u\{x\mid \alpha\}::\langle\beta\rangle,y=\beta,\alpha]] \end{array}$

$\begin{array}{l} \textbf{Def (power set). }\\ u:\mathsf{powerset}[u]=\\ x,x\in u\\\hline \mathsf{comprehension}[u,y\subseteq_u x,y],\{y\mid y\subseteq_u x\}=\mathsf{P}(x) \end{array}$

$\begin{array}{l} \textbf{Def (pairing). } \\ u:\mathsf{pairing}[u]=\\ x,y,x\in u, y\in u\\\hline \mathsf{comprehension}[u,z=x\;\mathsf{or}\;z=y,z],\{z\mid z=x\;\mathsf{or}\;z=y\}=\{x,y\} \end{array}$

$\begin{array}{l} \textbf{Def (union). }\\ u:\mathsf{union}[u]=\\ x,x\in u\\\hline \mathsf{comprehension}[u,[z,y\in_u z,z\in_u x],y],\{y\mid [z,y\in_u z,z\in_u x]\}=\mathsf{U}(x) \end{array}$

$\begin{array}{l} \textbf{Def (restricted comprehension). }\\ u:\mathsf{restrcompr}[u,\alpha]=\\ x,x\in u\\\hline \mathsf{comprehension}[u,[y\in_u x,\alpha],y],\{y\mid [y\in_u x,\alpha]\}=\{y\in_u x \mid \alpha\} \end{array}$