12/27/20
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)
Should you wish to use the Deriver application for this, see Exercises for Easy Deriver using the Deriver Web Application [Gentzen] . Good advice is: start these tutorials without it, but if you get to the point of wishing to save some work, then switch to the Deriver Web Application.
Then ... either copy and paste the above formulas into the Journal or use the Deriver File Menu to Open from URL... with this address https://softoption.us/test/Deriver/CombinedTutorialsGentzen.html .
Preferences
You will need to set some Preferences for this.
- set identity to true (and that will give you the identity rules)
- set setTheory to true (to get set theories)
- set firstOrder to true (to get first order theories)
- and you can check that the parser is set to gentzen.