[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents \section{Axiom of ordered pairing} For all sets $x$ and $y$, there exists a set $(x, y)$, such that for all $a \in x$ and $b \in y$, $(a, b) \in (x, y)$, and for all $c \in (x, y)$, there exist $\pi_1(c)$ and $\pi_2(c)$ such that $\pi_1((a, b)) = a$ and $\pi_2((a, b)) = b$. --- Literal basic stuff about high school algebra: * What is a variable? * What are free and bound variables? * What is substitution of terms for variables? \section{Variables} A variable is a symbol $x$ which represents an arbitrary instantiation of a type $T$. Variables are thus types and written as $x:T$. Variables are usually found in the context, as $\Gamma, x:T, \Delta \vdash \mathcal{J}$ for arbitrary judgment $\mathcal{J}$. \section{Free and bound variables} \section{Substitution} \section{Change of bound variables} category: redirected to nlab