Timeline for Kuratowski's definition of ordered pairs
Current License: CC BY-SA 3.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 4, 2012 at 14:45 | comment | added | David Fernandez-Breton | This "flat" pairing function described above is what some people know as "Quine's definition" of an ordered pair. en.wikipedia.org/wiki/Ordered_pair#Quine-Rosser_definition As far as I know, this is the definition used by people working in NF and similar theories, it has the advantage that every set is an ordered pair and so the functions first(-) and second(-) (projections) are total functions instead of partial ones. | |
| Apr 24, 2011 at 17:59 | comment | added | Carl Mummert | Flat pairing functions are particularly important in type theory. For example we can regard every set of natural numbers as a code for a pair of sets, without leaving second-order arithmetic. Similarly every set of sets of natural numbers can be viewed as a code for a pair of sets of sets, without leaving third order arithmetic. I have heard flat pairing functions are also useful for non-ZF set theories such as New Foundations, although I don't know much about that area. | |
| Apr 24, 2011 at 3:12 | history | answered | Joel David Hamkins | CC BY-SA 3.0 |