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)
If you decide to use the web application for the exercises you can launch it from here Deriver [Gentzen] — username 'logic' password 'logic'. Then either copy and paste the above formulas into the Journal or use the Deriver File Menu to Open Web Page 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 firstOrder to true (to get first order theories)
- set setTheory to true (to get set theory)
- and you can check that the parser is set to gentzen.