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.

$\newcommand{\fin}{\lfloor} \newcommand{\ass}{\lceil} \newcommand{\con}{|} \begin{array}{l} \textbf{Thm (Russell). }\\ \ass a,[b:[\beta*[b,a]::[\beta*[b,b]:\alpha]]]\\ \con \beta*[a,a]::[\beta*[a,a]:\alpha]\\ \con\ass \beta*[a,a]\\ \con\con \beta*[a,a]:\alpha\\ \con\fin \alpha\\ \con \beta*[a,a]:\alpha\\ \con \beta*[a,a]\\ \fin \alpha\\ a,[b,[\beta*[b,a]::[\beta*[b,b]:\alpha]]]:\alpha \end{array}$

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}$