Theorem 1

$x = x$.

Let $S$ denote the relation $x = x$ in $\mathscr{T}_0$. By C27 (§4, no. 1), for every relation $R$ in $\mathscr{T}_0$, $(\forall x)(R \Leftrightarrow R)$ is a theorem in $\mathscr{T}_0$, and therefore, by S7, $\tau_x(R) = \tau_x(R)$, that is to say $(\tau_x(R)|x)S$, is a theorem in $\mathscr{T}_0$. Taking $R$ to be the relation "not $S$" and considering C26 (§4, no. 1), we see that $(\forall x)S$ is a theorem in $\mathscr{T}_0$. By C30 (§4, no. 3), $S$ is therefore a theorem in $\mathscr{T}_0$.

The relation $(\forall x)(x = x)$ is also a theorem in $\mathscr{T}_0$; and if $T$ is a term in $\mathscr{T}_0$, then $T = T$ is a theorem in $\mathscr{T}_0$ (cf. §4, no. 3). It is possible to transform later theorems in the same way into theorems in which no letter appears or into metamathematical criteria. From now on we shall not explicitly perform these transformations, but we shall often implicitly make use of them.