12/31/13
Order and Ordered pairs
Thus far nothing we have done has order in it. We are definitely going to need the notion order, both for mathematics and everything else. In mathematics, on a simple two dimensional graph the point with x=1 and y=2 is not the same as the point with x=2 and y=1. In the world at large John being taller than Jane is not the same as Jane being taller than John. Set theory is going to need an approach to order.
The notation <x,y> is used for ordered pair, and conceptually it is a set, so formulas like <x,y>εz and zε<x,y> are well formed formulae.
The key point about ordered pairs is that two of them are equal to each other iff their first coordinates are equal and their second coordinates are equal ie
(<x,y>=<w,v>) ≡ (x=w∧y=v)
We need to have this available within our set theory. There are two ways to do this. There could be another axiom which just allows us this. Or we could find a definition that has exactly these properties. The former is clear, but adds an axiom. The latter is more frugal but can be, and typically is, a little obscure or odd in its details. Most set theories do the latter, then the definition they choose is
<x,y> = df. {{x},{x,y}}
We that definition we can proove the property we want ie
({{x},{x,y}}={{w},{w,v}}) ≡ (x=w∧y=v)
∴({{x},{x,y}}={{w},{w,v}}) ≡ (x=w∧y=v)