12/15/20
With two sets, say x and y, there are various ways they can be put together.
There is the union of the two sets, symbolized with ∪, which the set formed when elements are members of one set or the other
zε(x∪y) ≡ (zεx∨zεy) Axiom of Union
zε(x∪y) :: (zεx∨zεy) Union Rewrite
There is the intersection of the two sets, symbolized with ∩, which the set formed when elements are members of one set and the other
zε(x∩y) ≡ (zεx∧zεy) Axiom of Intersection
zε(x∩y) :: (zεx∧zεy) Intersection Rewrite
There is the (relative) complement of the two sets, symbolized with -, which the set formed when elements are members of one set and not the other
zε(x-y) ≡ (zεx∧z∉y) Axiom of Complement
zε(x-y) :: (zεx∧z∉y) Complement Rewrite
Unordered pairs, singletons, triples, etc.
When we introduced the notation {a,b,c}, for example, to illustrate a set by extension, we did not really say what the notation meant. What it means, in the case of {a,b,c}, is the set of those things that either equal a or equal b or equal c.
We can be more formal about this using another axiom-- the Axiom of Pairs-- and a series of definitions. First the axiom tells us what a pair is:
zε{x,y} ≡ (z=x∨z=y) Axiom of Pair
zε{x,y}:: (z=x∨z=y) Pair Rewrite
This notation {x,y} tells us that there is a set, usually with two members in it, namely x and y. And for something to be in the set that thing has either to equal x or to equal y.
An important point here is that there is no order to this. There is no notion of a 'first' member of the set and a 'second member' of the set, for
zε{x,y} is equivalent to (z=x∨z=y) is equivalent to (z=y∨z=x) is equivalent to zε{y,x}
Yet again this axiom might have been introduced by the Axiom Schema of Specification and the notation{x,y}.
{x,y} usually has two members in it. But there is the possibility that x=y ie that the 'two' are actually one, the x and y are two names or aliases for the same one identical thing. {x,x} has only one member, namely x. So now there is a definition
{x}=df.{x,x}
Then we can get sets with 3 or more members just by union-ing together what we have got.
{x,y,z}=df.{x,y} ∪{z}
And similarly for more
{x,y,z,w}=df.{x,y,z} ∪{w}
Sometimes, when doing proofs, we can be shorten this by using instances the Axiom Schema of Specification directly with definitions
{}= ∅
{y}={x:(x=y)}
{y,z}={x:(x=y∨x=z)
{y,z,w}={x:(x=y∨x=z∨x=w)}
{y,z,w,v}={x:(x=y∨x=z∨x=w∨x=v)}
etc.
The software does not have the meaning of this notation built in. It does have the Axiom of Pairs (and the Schema of Specification). So it is good directly for pairs eg {a,b}. But if you want to do proofs with singletons, triples etc using the {} notation you'll need to add suitable definitions as premises (we do so in one of the Exercises below).
Power Set
The Power Set of a (single) set is the set of all subsets of that set, for the set x, this is symbolized with ℘(x)
zε ℘(x) ≡ (z⊂x) Axiom of Power Set
zε ℘(x) :: (z⊂x) Power Set Rewrite
Power Sets are 'large' sets-- they have (2 to the power n) members if the original set has n members. (So if a set has 2 members, its power set has 4 members; if a set has 10 members its power set has 1024 members.)
Exercise 1(of 3)
Exercise 2(of 3)
Exercise 3(of 3)
Video of Example 1 being done.
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.