Implementation of mathematics in set theory: Difference between revisions

Revision as of 01:43, 24 January 2013

Revision as of 07:25, 24 January 2013

Line 265:

In this class of constructions it appears that [[ZFC]] has an advantage over [[New Foundations|NFU]]: though the constructions are clearly feasible in [[New Foundations|NFU]], they are more complicated than in ZFC for reasons having to do with stratification.

Throughout this section assume a type-level ordered pair. Define <math>(x_1,x_2,\ldots,x_n,x_{n+1})</math> as <math>(x_1,(x_2,\ldots,x_n))</math>. The definition of the general ''n''-tuple using the Kuratowski pair is trickier, as one needs to keep the types of all the projections the same, and the type displacement between the ''n''-tuple and its projections increases as ''n'' increases. Here, the ''n''-tuple has the same type as each of its projections.

General cartesian products are defined similarly: <math>A_1 \times A_2 \times \ldots \times A_n = A_1 \times (A_2 \times \ldots \times A_n)</math>