Fix a countably infinite set of variables, inductively define the set of terms over a pca $\mathcal{A}$:

1. a variable is a term,
2. an element of $\mathcal{A}$ is a term,
3. given two terms $s$ and $t$, we may form a new term $s\ t$.

A closed term is defined if, when we interpret $s\ t$ as $s$ applied to $t$ in $\mathcal{A}$, all these applications are defined.

Extends to open term $t$ then is if all possible substitutions of all variables in $t$ by elements of $\mathcal{A}$, the obtained closed term is defined.

For a variable $x$ and a term $t$, we can define a new term $\langle x \rangle.\ t$ by recursion on terms:

• $\langle x \rangle.\ x \doteq I = S\ K\ K$,
• $\langle x \rangle.\ y \doteq K\ y$ if $y$ is a variable different from $x$,
• $\langle x \rangle.\ a \doteq K\ a$ for $a \in \mathcal{A}$,
• $\langle x \rangle.\ (t_1\ t_2) \doteq S(\langle x \rangle.\ t_1)(\langle x \rangle.\ t_2)$.

$\langle xy \rangle.\ t$ writes for $\langle x \rangle.\ (\langle y \rangle.\ t)$

Now, we can work on it, e.g.

so

Pair and projections are