1/9/09
There is a shorter and quicker proof using rewrite rules. Ordinarily there is a lot of messing around with instantiating quantifiers, renaming bound variables, etc.. Rewrite rules avoid much of this (and so we can concentrate on Set Theory). You might want to remind yourself of Rewrite Rules and its video.
1/9/09
This is a long proof using axioms. There is a shorter and quicker way using rewrite rules.
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' .
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.
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
Possible background reading:
Halmos, Paul R. [1960] Naive Set Theory (this is the standard text for this kind of material)
Sowa, John F. [2000] Knowledge Representation pp.98-103
Keene G.B. [1974] Formal Set Theory
Wikipedia Naive Set Theory
Formal Number Theory. Just more theorems for you.
Formal Number Theory has five proper symbols {=,',+, .,0} and six proper axioms
(∀x)(∀y)(x'=y'⊃x=y),
(∀x)~(x'=0),
(∀x)(x+0=x),
(∀x)(∀y)(x+y'=(x+y)'),
(∀x)(x.0=0),
(∀x)(∀y)(x.y'=x.y+x)
And the axiom (metalanguage) schema of induction. If φ[n] is any formula in the object language with free variable n then
(φ[0]∧(∀n)(φ[n]⊃φ[n'])) ⊃ (∀n)φ[n]
The logic we are mainly occupied with here is first-order logic (sometimes called first order predicate calculus (with functional terms and identity)). A case can be made that it is the main, or the one true, logic. Sowa writes:
2013
To learn about the Uniqueness quantifier (a part of identity), and to be introduced to definite descriptions.
Uniqueness is central in mathematics, and definite descriptions is a core area in philosophical logic.