Anacona et al (2014) point out that Bourbaki Theory of Sets (1968) lacks the Foundation Axiom. Moreover, the authors remark that the expressive power of Bourbaki Theory of Sets is equivalent to the class theory of NBG.
Given that NBG is a conservative extension of ZFC and given the missing Foundation Axiom, I'm wondering if in Bourbaki Theory of Sets it is possible to prove the Anti-Foundation Axiom, which can be stated as either:
(AFA$_{1}$): Given any extensional binary relation ≺ on any set S, there exists a unique transitive set U such that (U,∈) is isomorphic (necessarily uniquely) to (S,≺).
(AFA$_{2}$): Every accessible pointed graph has a unique decoration.
I would like to ask you if someone could help me to see how the proof would work based on the axioms of Bourbaki Theory of Sets:
- Axiom of Global Choice (in the syntactic manner of Hilbert's $\varepsilon$-operator)
- Axiom of Extensionality
- Axiom of Subsets
- Axiom of Unions
- Axiom of Ordered Pairs
- Axiom of Infinity
- Axiom of Replacement
I hope my hypothesis is clear. However, I acknowledge that this information might be not enough to formulate a proof, so please feel free to ask me any clarificatory question.
Best Answer
No, they do not prove either of those antifoundation axioms (or anything else which could reasonably be called an antifoundation axiom).
This is because those axioms are consistent with the axiom of foundation. Therefore they don't disprove foundation. But any antifoundation axiom implies the negation of foundation - that's sort of the point - and so a fortiori your axioms can't prove any antifoundation axiom.
(Of course this all assumes they're consistent in the first place!)