12/25/20
There is the notion that whenever an element is a member of one set then it is also a member of a second set. When this occurs the first set is said to be a subset of the second, and this is denoted by the symbol '⊂' . There is an axiom covering this
(x⊂y) ≡(∀z)(zεx⊃zεy) Axiom of Subsets
In English this says, 'x is a subset of y if, and only if, All z, if z is a member of x then z is also a member of y' .
[We certainly could have established this by means of a definition and the Axiom Schema of Abstraction, as explained earlier.]
And now we (ie you) can prove some theorems
1. ∴ ((u⊂v)∧ (v⊂w))⊃ (u⊂w) /*The transitivity of the subset relation. Help Video on how to do this.*/
2. ∴ ((u⊂v)∧ (v⊂u))⊃ (u=v) /*If two sets are subsets of each other, they are equal to each other.*/
3. ∴ (u=v)⊃ ((u⊂v)∧ (y⊂v)) /*If two sets are equal to each other, they are subsets of each other.*/
You will find the Axioms for Set Theory under the Advanced Menu, and all 3 of these proofs involve Universal Genalization and Instantiation steps to get the variables with the names you want.
Here is a proof of theorem 1.
Learning even more from mathematicians on making our proofs simpler
There is an awkwardness in our formal apparatus. It is to do with the facts that often we want to use xs and ys in our formulas, and that our axioms also use xs and ys; this sometimes forces us into 'changing bound variables' and all sorts of purely formal manipulations. These formal steps are nothing to do with set theory (and, in fact, are a waste of time as far as learning set theory goes). [The difficulties here are the reason why us, vs and ws were used in Theorems 1-3.]
When working mathematicians look at, say
(x⊂y) ≡(∀z)(zεx⊃zεy) Axiom of Subsets
they know that the xs and ys can have, or be instantiated to, any values. They see the xs and ys as being patterns and then those patterns can be matched to any values. We can do the same. We can take the Axiom of Subsets (and the Axiom of Extensionality) to be rewrite rules. So here are the rules.
(x=y)::(∀z)(zεx≡zεy)) Rewrite Extensionality
(x⊂y)::(∀z)(zεx⊃zεy) Rewrite Subsets
[You might want to revise earlier material on rewriting. Easy Deriver Rewrites. Rewrite Rules are found on the Advanced Menu under Rewrites.]
Here is the same theorem using rewrites
And here is a Help Video showing that.
To continue with Set Theory
[There is a point of notation. When one set is a subset of another, often it is possible for the first to actually equal the second. Some writers acknowledge this by using the symbol '⊆' so that a⊆b is read 'a is a subset of b or is equal to it'; then '⊊' as in a⊊b is 'a is a subset of b but is not equal to it'. If a set is a subset of another but is not equal to it, the first is said to be a proper subset of the second. We are not using any of these conventions here. For us, a⊂b is 'a is a subset of b or is equal to it' and a⊂b∧~(a=b) says that 'a is a proper subset of b' (for it is a subset and it is not equal).]
There is the empty or null set. This is a set that nothing is a member of, it has the symbol '∅' .
(∀x)(x∉∅) Axiom of Empty Set
In English this says, 'Nothing is a member of the empty set'. [There is the alternative notation of '{}' for the empty set-- we are not really using that here. The software will read {} but it does not know that (∀x)(x∉{}). So, if you want to use that convention in your proofs, you will need an extra premise that ∅={} .]
There is a symbolic convention in use here 'not a member of' has the symbol '∉' so, for example, ~(xε∅) can be abbreviated as (x∉∅) .
There is the universe or universal set. This is a set that everything is a member of, it has the symbol 'Ü' (this is the German U-umlaut symbol and it is typed by following option-u with uppercase-U). [An aside: Most books will use upper case-U i.e. U for the universal set, but we already have U as a predicate (and as a proposition, and as a relation...). So this convention would mean that 'UU' would be well formed (say 'the Universe is unpleasant'), so would 'UUU' (say 'the Universe it underneath itself') and so on. Now the Universal symbol is a constant, whereas predicates are predicates i.e. they are of different type. It seems better to keep that clear, and one way is to use Ü for the universal set.]
(∀x)(xεÜ) Axiom of Universe Set
In English this says, 'Everything is a member of the Universal set' .
More theorems
4. ∴ ∅⊂x /*The Empty set is a subset of every set. */
5. ∴ x⊂Ü /*Every set is a subset of the Universe set.*/
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.