Exercise 6, § 1

This solution was written by laguna-s-2.1-free and judged by a machine. It is not Bourbaki's and it has not been checked by a person.

Given that $A$ and $\Rightarrow AB$ are relations in the theory $\mathscr{T}$, we need to show that $B$ is a relation in $\mathscr{T}$. Here, $\Rightarrow AB$ denotes the assembly $\vee \neg A B$, as specified (see the Remark after CF5: $\Rightarrow AB$ represents $\vee \neg A B$). Since $\Rightarrow AB$ is a relation, it must be constructed through condition (c) of formative constructions, which requires both constituents $\neg A$ and $B$ to be relations. Given $A$ is a relation, $\neg A$ is a relation by CF2, so the first component $\neg A$ is confirmed as a relation. However, for the disjunction $\vee \neg A B$ to be valid, the second component $B$ must also be a relation because both components of a disjunction must be second-species assemblies (relations).

To confirm that $B$ cannot be a term, suppose for contradiction that $B$ is a term (first species). A term is an assembly of the first species, and by Exercise 4, the assembly $AB$ (with $A$ a relation and $B$ a term) cannot be a term or a relation. However, constructing $\Rightarrow AB$ as $\vee \neg A B$ directly involves $B$ as the second component. Since $B$ is a term (first species), this would violate condition (c) of formative constructions, as only relations (second species) can be components of disjunctions. Thus, $B$ cannot be a term. Therefore, $B$ must itself be a relation; this follows directly from the definitions of formative constructions and criteria CF1 and CF2, combined with Exercise 4 to exclude $B$ as a term.