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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.