1

Trying to understand the proof (or rather, verification) of the following criterion of formation in Bourbaki, Chapter 1 (p. 22 here):

CF7. Let $A$ be a relation (term), and let $x$ and $y$ be letters. Then $(y|x)A$ is a relation (term).

Let $A_1, A_2, \dots, A_n$ be a formative construction in which $A$ appears. We shall show step by step that, if $A_t$ is a relation (term) then so is $(y|x)A_t$.

Suppose that this point has been established for $A_1, A_2, \dots, A_{i-1}$; let us prove it for $A_i$. If $A_i$ is a letter, then $(y|x)A_i$ is a letter, etc.

They proceed similarly for the case where $A_i$ is the negation of a relation that preceeds it in the formal construction, and so on, so that every criterion to be a formula/term (here, that it must be part of a formative construction) is checked.

I realize it is reminiscent of induction, yet I do not quite understand why it is done that way. First of all, is $A_t$ supposed to correspond to $A$? Then why resort to $A_{i-1}$ instead of $A_{t-1}$? In fact, I am not quite understanding why they "assume that this point has been established for" the steps up to $i-1$.

Could anybody sort that out for me in simpler terms? (and no, I am not trying to learn Set Theory from Bourbaki, but mainly trying to see how sound the first Chapter is for other purposes). Thanks.

itsqualtime
  • 119
  • 7

1 Answers1

1

Apart from the "unusual" terminology, the proof is a standrd proof by induction on the formation sequence (here : formative construction) of a term or formula (here : relation).

On the basis of the definition [page 19] of formative construction, the proof proceeds assuming that the property holds for all $k < i$ (i.e. for $A_1, A_2, \ldots, A_ {i-1}$) and the induction step proves it for $i$.

I.e. we have to prove that $(y|x)A_i$ is a relation or term.

The proof is by cases, according to the five cases ((a) to (e)) of the definition [page 19] :

(a) if $A_i$ is a letter, then $A_i'$ (that is $(y|x)A_i$) also is;

(b) There is in the sequence an assembly of the second species $A_j, j < i$, such that $A_i$ is $\lnot A_j$.

[...].

Note

There is no "magic": $A_t$ plays no special role; it's only a way of to refer to the "generic" term of the formative construction.

Community
  • 1
Mauro ALLEGRANZA
  • 94,169
  • but is it sound to assume that this holds for each step of the sequence all the way up to $i-1$? See, a standard induction would show that CF7 holds for $A_0$ say (or is it omitted just because it is so trivial?), and then proceed by showing that if it is true of some $i$, then it must hold for $i+1$ as well.

    I realize that this just could be a different way of applying induction (that is, the inductive steps do not correspond with the formative sequence steps), I'm just not quite seeing it yet.

     – itsqualtime Oct 13 '14 at 23:19
  • and, is induction necessary here? (even though it's technically not a proof but rather a verification) – itsqualtime Oct 14 '14 at 00:27
  • @itsqualtime - There are different equivalent formulation of Mathematical induction; the version used is : "complete induction [that] uses the hypothesis that the statement holds for all smaller $n$ more thoroughly." – Mauro ALLEGRANZA Oct 14 '14 at 06:20
  • Mauro, one more question if I may. In terms of the strong induction as defined here on the first slide: http://www.youtube.com/watch?v=ML-g2xLYruE how would you write out explicitly the basis and inductive step here use by Bourbaki in the same format? Just want to make sure I'm getting the basis step right. Would it necessary have to be a term, since you can start a formative construction with a formula right away? THanks. – itsqualtime Oct 15 '14 at 01:40
  • You have to "separate" two facts : the induction on the "number" $i$ of the formula or term $A_i$ in the formative sequence from the five cases to be considered for each $A_i$; in general, each $A_i$ con be a term or the negation of a preceding term in the sequence or ... – Mauro ALLEGRANZA Oct 15 '14 at 07:47