# Bourbaki: Use of tau choice operator?

I have a question about evaluating truth of the sign assemblies in Bourbaki Theory of Sets.

It's my understanding that when there are duplicate assemblies each starting with the choice operator $$\tau$$, this operator must choose the same value for each linked $$\square$$ in all duplicate assemblies. Therefore, to evaluate the truth of a sequence of signs, the sequence must be searched for duplicate sequences starting with $$\tau$$.

Is it documented elsewhere? I suspect this is costly, but are there advantages? Perhaps eliminating the variable name from the form so duplicates can be found?

I have yet to see any Bourbaki documentation on this and am confused by that.

• See ARD Mathias, "A term of length 4 523 659 424 929" (2002) – Mauro ALLEGRANZA Apr 13 at 14:21
• Maybe they expected a finite automata (Turing Machine) to recognize or prove, one that does not depend on the theory of their book – Nick Apr 14 at 23:06
• Of course this is documented by Bourbaki. It is essentially the meaning of axiom scheme S7. – Fred Rohrer May 6 at 11:34