Implementation of mathematics in set theory: Difference between revisions

Content deleted Content added
Line 295:
In [[NFU]], the main difficulty is that <math>[x]_R</math> is one type higher than x, so for
example the "map" <math>x \mapsto [x]_R</math> is not in general a (set) function (though <math>\{x\} \mapsto [x]_R</math> is a set). This can be circumvented by the use of the Axiom of Choice to select
a representative from each equivalence class to replace <math>[x]_R</math>, which will be at the same type as x, or by choosing
a canonical representative if there is a way to do this without invoking Choice (the use
of representatives is hardly unknown in [[ZFC]], either. In [[NFU]], the use of equivalence