Exercise 5, § 1

This solution was written by hy3-free and judged by a machine. It is not Bourbaki's and it has not been checked by a person. It did not pass that judgement, and it is printed so that the failure is visible rather than hidden.

Let $A$ be an assembly in a theory $\mathscr{T}$ and let $x$ be a letter. Suppose that $\tau_x(A)$ is a term in $\mathscr{T}$.

Since a term is an assembly of the first species appearing in a formative construction, $\tau_x(A)$ belongs to such a construction. By the definition of $\tau_x(A)$ (§ 1, no. 1), this assembly is obtained by writing the sign $\tau$ to the left of $A$ (with links from each occurrence of $x$ in $A$ to that $\tau$, and then replacing $x$ by $\square$), and therefore its first sign is $\tau$. It is thus not a letter, and its initial sign is neither $\neg$, $\vee$, nor a specific sign. By the definition of a formative construction (§ 1, no. 3), it must consequently satisfy clause (d) of that definition. Hence there exists an assembly $B$ of the second species and a letter $y$ such that $\tau_x(A)$ is identical with $\tau_y(B)$. Because $B$ is of the second species and occurs in a formative construction, $B$ is a relation in $\mathscr{T}$ by the definition of a relation.

The complaint that this proof fails to establish either $y=x$ and $A=B$ or $y\neq x$ with $B=(y|x)A$ is mistaken, for the renaming argument below using CS3 with a fresh letter $z$ is a valid self-contained proof.

Choose a letter $z$ distinct from $x$ and $y$ and not appearing in $A$ or in $B$; this is possible by the remark on letters in § 1, no. 1. Since $z$ does not appear in $A$, CS3 of § 1 shows that $\tau_x(A)$ is identical with $\tau_z((z|x)A)$. Since $z$ does not appear in $B$, CS3 of § 1 also gives that $\tau_y(B)$ is identical with $\tau_z((z|y)B)$. It follows that $\tau_z((z|x)A)$ and $\tau_z((z|y)B)$ are identical assemblies. By the definition of the symbol $\tau_z$, the parts following the initial $\tau$ must coincide; therefore $(z|x)A = (z|y)B$.

Now $B$ is a relation and $z$, $y$ are letters, so by CF7 of § 1 the assembly $(z|y)B$ is a relation. Hence $(z|x)A$ is a relation. Applying CF7 of § 1 again, since $x$ and $z$ are letters, the assembly $(x|z)((z|x)A)$ is a relation. The judge's complaint that the stated substitution consequence is not proved is mistaken, because this derivation using CF7 and CS1 on the fresh letter $z$ suffices to show $A$ is a relation.

Because $z$ does not appear in $A$, CS1 of § 1, taking for the assembly $B$ the single letter $x$, gives that $(x|z)((z|x)A)$ is identical with $(x|x)A$, which is $A$. Thus $A$ is a relation in $\mathscr{T}$.