Theory of Links Axioms

Language defined in this other blog post.

WORK IN PROGRESS, SUBJECT TO CHANGE

Axioms for the ∈ relation:

Axiom of extensionality for non-link objects (changed to not imply that all members of $U_L$are equal): ∀x∀y((x∈$U_L$)$\lor$(y∈$U_L$)$\lor$((∀z((z∈x)$\leftrightarrow$(z∈y)))$\rightarrow$x=y))

Axiom of regularity: ∀$x_1$(∃$x_2$($x_2$∈$x_1$)$\rightarrow$∃$x_{3}$∈$x_1$(¬∃$x_{4}$($x_{4}$∈$x_1$$\and$$x_{4}$∈$x_{3}$)))

Axiom of pairing: ∀$x_1$∀$x_2$∃z∀y(y∈z$\leftrightarrow$(y=$x_1$∨y=$x_2$))

Axiom of union: ∀$x_1$∃$x_2$∀$x_{3}$($x_{3}$∈$x_2$$\leftrightarrow$∃$x_{4}$($x_{4}$∈$x_1$∧$x_{3}$∈$x_{4}$))

Axioms for $\vec{w}$, ${\vec {uw}}$, ${\vec {ruw}}$, ${\vec {rswr}}$, and $\vec s$ relations (originally introduced by P進大好きbot in User blog:P進大好きbot/Rayo name of 65536#Wedge):

Axiom of Wedging: ∀x∀y∀z($\vec{w}$(x,y,z)$\leftrightarrow$(y$\ne$z$\and$∃$x_2$((y∈$x_2$$\and$z∈$x_2$)$\and$$x_2$∈x))))

Axiom of Uniquely Wedging: ∀x∀y∀z(${\vec {uw}}$(x,y,z)$\leftrightarrow$($\vec{w}$(x,y,z)$\and$(¬∃$x_2$((z$\ne$$x_2$$\and$$\vec{w}$(x,y,$x_2$))))))

Axiom of Restriction Of Uniquely Wedging: ∀x∀y∀z(${\vec {ruw}}$(x,y,z)$\leftrightarrow$∃$x_2$($x_2$∈y$\and$${\vec {uw}}$(x,$x_2$,z)))

Axiom of Restriction Of Having Surjective Wedge Relation: ∀x∀y∀z(${\vec {rswr}}$(x,y,z)$\leftrightarrow$¬∃$x_2$($x_2$∈z$\and$¬${\vec {ruw}}$(x,y,$x_2$)))

Axiom of Surjection: ∀x∀y((x$\vec s$y)$\leftrightarrow$∃z(${\vec {rswr}}$(z,x,y)))

Axiom for the $\cong$ relation:

Axiom of Equal Cardinality: ∀x∀y((x$\cong$y)$\leftrightarrow$(((x$\vec s$y)$\and$(y$\vec s$x))$\lor$x=y))

Axiom for the $\doteqdot$ relation:

Axiom of unordered pair: ∀x((x$\doteqdot$)$\leftrightarrow$∃y ∈x(∃z ∈x(y$\ne$z$\land \neg$(∃$x_2$ ∈x(y$\ne$$x_2$$\and$z$\ne$$x_2$)))))

Axiom for the ${\widehat {\in }}$ relation:

Axiom of one element from each set in unordered pair: ∀x∀y∀z(${\widehat {\in }}$(x,y,z)$\leftrightarrow$(x$\doteqdot$$\and$∃$x_2$∈x($x_2$∈y$\and$∃$x_{3}$∈x($x_{3}$∈y$\and$$x_2$$\ne$$x_{3}$))))

Axiom for the $\in _{\doteqdot }$ relation:

Axiom of containing only unordered pairs: ∀x((x$\in _{\doteqdot }$)$\leftrightarrow$∀y∈x(y$\doteqdot$))

Axiom for the $\subseteq _{\in }$ relation:

Axiom of double containing all elements: ∀x∀y(x$\subseteq _{\in }$y$\leftrightarrow$∀z∈x(∃$x_2$∈y(z∈$x_2$)))

Axiom for the $\vec{m}$ relation:

Axiom of map: ∀x∀y∀z($\vec{m}$(x,y,z)$\leftrightarrow$(x$\cong$y$\and$y$\cong$z$\and$x$\in _{\doteqdot }$$\and$(∀$x_2$∈x(${\widehat {\in }}$($x_2$,y,z)))$\and$y$\subseteq _{\in }$x$\and$z$\subseteq _{\in }$x))

Axioms for the $\subseteq$ relation:

Axiom Of Subsets: ∀x∀y(y$\subseteq$x$\leftrightarrow$∀z(z∈y$\rightarrow$z∈x))

Axiom of the Power Set: ∀x∃y∀z(z$\subseteq$x$\leftrightarrow$z∈y)

Axiom for the $\cup$ function:

Axioms of Union: ∀x∀y∀z((z∈(x$\cup$y))$\leftrightarrow$((z∈x)$\lor$(z∈y))

Axiom for the $\cap$ function:

Axiom of Intersection: ∀x∀y∀z((z∈(x$\cap$y))$\leftrightarrow$((z∈x)$\and$(z∈y))

Axiom for the S function:

Axiom of Successor: ∀x∀y((y∈Sx)$\leftrightarrow$((x=y)$\lor$(x∈y)))

Axioms for the 🔗 relation:

Axiom of link extensionality: ∀x∈$U_L$∀y∈$U_L$((∀z∈$U_L$((x🔗z)$\leftrightarrow$(y🔗z)))$\rightarrow$x=y)

Axiom of Commutativity: ∀x∈$U_L$∀y∈$U_L$((x🔗y)$\leftrightarrow$(y🔗x))

Axiom of Separate Links: ∀x$\subseteq$$U_L$(∃y∈$U_L$(∀z∈x((((¬(x=$U_L$))$\rightarrow$(¬(y=z)))$\and$¬(y🔗z))))

Axiom of Link Existence to Alternate Set of Links:

$\forall x_{1}\subseteq U_{L}(\forall x_{2}\subseteq x_{1}(\exists x_{3}(\forall x_{4}\in x_{3}\forall x_{5}\in x_{3}(\exists x_{6}\in x_{4}(x_{6}\in x_{1}\land \forall x_{7}\in x_{4}(x_{7}\in U_{L}\land \neg (x_{6}=x_{7}$

$\leftrightarrow (\forall x_{8}\in x_{4}(x_{6}=x_{8}\lor x_{7}=x_{8})\land \neg (x_{7}\in x_{1})))))\land \forall x_{9}\in x_{4}\forall x_{10}\in x_{4}\forall x_{11}\in x_{5}\forall x_{12}\in x_{5}(((x_{9}$

$\in x_{1})\land (x_{11}\in x_{1})\land \neg ((x_{9}=x_{10})\lor (x_{11}=x_{12})))\rightarrow ((x_{9}$🔗$x_{11})\leftrightarrow (x_{10}$🔗$x_{12}))))\land \exists x_{13}\in U_{L}($

$\forall x_{14}\in x_{3}(\forall x_{15}\in x_{14}\forall x_{16}\in x_{14}(((x_{15}\in x_{2})\leftrightarrow (x_{13}$🔗$x_{16}))))))))$

Axiom of emptiness: ∀x∈$U_L$∀y(¬(y∈x))

Axiom of if sets can link: ∀x((¬(x∈$U_L$))$\rightarrow$∀y(¬(x🔗y)))

Other axiom:

Axiom of infinity which contains no link: ∃$x_1$(∃y∈$x_1$(¬∃z(z∈y))$\and$∀$x_2$∈$x_1$(S$x_2$∈$x_1$)$\and$¬∃y∈$x_1$(y∈$U_L$))