Bourbaki Proof in First Consequences? Use of Not?

Question

In Bourbaki Theory of Sets English (c) 1970 Section 3.2 C6 there is a first consequence that I have questions about. I have attached images of the text here. My question is:

• We are told that A, B, C are are relations in Theory. So $\vdash A, B, C$. How can "not A" be substituted into S4 when it is not defined yet as a true relation of the theory or axiom? Is $\vdash \lnot A$ added as a step in this proof?

• Where does Bourbaki define what "not A" is? I have only found use regarding the symbol $\lnot$ on Page 24 Section 2 and that is all up to the point of this first consequence.

I am new to proof theory, however understand how the substitutions lead to the conclusion. I'm just concerned about the above being properly defined.

Thanks

C6 Proof Axioms

Answer 1

We are told that $A, B, C$ are are relations in Theory. So $⊢A,B,C$. How can "not $A$" be substituted into S4 when it is not defined yet as a true relation of the theory or axiom?

In Bourbaki's text, relations [i.e. assemblies of second species, §1.3] are formulas .

And see §2.2. : "A theorem in $\mathscr T$ is a relation which appears in a proof of $\mathscr T$".

Theorem C.6 asserts that "$A,B,C$ are relations in $\mathscr T$", i.e. formulas of the theory and not theorems.

S4 : $(A \to B) \to ((C \lor A) \to (C \lor B))$ is an axiom schema; thus, every instance of it is valid (a tautology).

This means that we can freely substitute the schematic letters : $A,B,C$ with formulas : again, the poof does not assume that $\lnot A$ is a theorem of $\mathscr T$.

Where does Bourbaki define what "not $A$" is?

See §1.4.CF2 : "If $A$ is a relation in a theory $\mathscr T$, then $\lnot A$ is a relation in $\mathscr T$.