12/24/20
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
Set theory is a basic mathematical theory or even a foundation of mathematics. Most everyone doing mathematics, or logic, needs to know at least some set theory. What they need to know is Naive Set Theory. Naive Set Theory is simple and adequate for most circumstances, but, unfortunately, it is also inconsistent (as we will see). This inconsistency has led to the proposal of any number of axiomatic set theories, which are very much the province of experts (we will avoid the axiomatic set theories).
Introductory set theory, say for mathematicians or, more especially for philosophers or philosophers of mathematics, really needs to cover three areas: some set theory in general, ordered pairs, and Russell's paradox via the axiom of specification or comprehension.
1. Introduction
Set theory deals primarily with sets, which are collections of items, and set membership, which is a relation between items and sets. Sets can be identified in many ways. In the First Order Logic using here, any of the constants or variables that we have eg x, y, z, a, b, c etc. can be thought of, in this setting, as being names of sets. It is also often quite useful to identify what is in a particular set. One way of doing this is by listing the items using the following notation
{a,b,c}
the curly brackets tell you it is a set and the comma separated list just picks out its members. An item can be said to be a member of set using the mathematical symbol for 'is an element of' (or the Greek letter epsilon); so
a ε {a,b,c}
says that the item 'a' is a member of the set {a,b,c} and this is a true statement.
1ε {a,b,c}
says that the item '1' is a member of the set {a,b,c} and this is a false statement.
We can use identity to let or define, say,
x= {a,b,c}
and then the statement
a ε x
would be true.
2. Building sets: the Axiom of Abstraction (or Specification, Comprehension, or Intension)
Thus far, when we have tried to say what is in a set, we have used notation like
{a,b,c}
and this picks out the set whose members are a, b, and c. It does so by extension.
But there are more general ways of doing this. In English, we could say, for example 'the set of all men'. What is happening here is that we are taking a property (or predicate) 'x is a man' and then forming a set of all the xs that satisfy this. There is a notation for this
{x:Mx} (or, alternatively, {x|Mx}) /*where Mx is the formal predicate for 'x is a Man'*/
This notation is sometimes called an abstraction, and what we are doing here is defining a set by intension.
So, for instance,
{a,b,c} is the definition of a particular set by extension
{x: x is one of the first three letters of the alphabet, lower case} is a definition of the same set by intension
{x:( x=a∨x=b∨ x=c) } is better definition of the same set by intension
[Abstractions are read like this. {x:Mx} is 'the set of xs such that Mx' . ]
Abstractions are sometimes called specifications, or comprehensions or intensions, or even set builders.
To explain how the formal apparatus is going to work, let us look at an analogy to this notation from ordinary predicate logic, that of Universally Quantified formulas and the logic rule of Universal Instantiation. For that we have a formula like
(∀x)(Fx⊃Gx) and Universal Instantiation will give us
(Fa⊃Ga)
With this, we have the 'binding variable of quantification', x in (∀x), and the 'scope' of the quantifier (Fx⊃Gx) and the instantiation consists of taking the scope and substituting the instantiating constant, a, for free occurrences of the variable x, throughout.
Going back to set abstractions, in
{x:Mx}
you can think of x as being the 'binding variable of quantification' and 'Mx' as being the 'scope'. Now, the scope can actually be much more general than just a predicate; in fact, in can be any formula of predicate logic (usually with a free x in it). So, for example
{x:(Fx⊃Gx)}
is a perfectly good abstraction.
When it comes to deciding whether something is a member of a set described by an abstraction: they are, if and only if, they satisfy (or are a substitution instance of) the scope. So, Fred is a member of {x:Mx}, iff, Fred is a Man. This principle can be written out as an Axiom Schema
(∀y)(yε{x:Φ[x]}≡Φ[y])
Axiom Schema of Abstraction (or Specification or Comprehension). The Set Builder Axiom Schema.
This is a 'schema' because the Φ is a variable or placeholder that stands for (nearly) any formula of predicate logic. So here are a few example instances of the Axiom Schema.
(∀y)(yε{x:Mx}≡My)
(∀y)(yε{x:x=a}≡(x=y))
(∀y)(yε{x:( x=a∨x=b∨ x=c)}≡(y=a∨y=b∨ y=c))
Then, to use these, we just instantiate the (∀y) to whatever we want. So, for example, were we to allow 'fred' as being a constant in our logic, the first instance of the schema could be instantiated to
fredε{x:Mx}≡Mfred /*ie Fred is a member of the set of xs such that x is a man iff fred is a man*/
[Let us go back to our analogy with Universal Instantiation, for one moment. The substitution instantiation there has to be 'legitimate', there cannot be any 'capturing' of variables. So, an instantiation like this is not permitted
(∀x)(∀y)(Fx⊃Gy) and Universal Instantiation will NOT give us
(∀y)(Fy⊃Gy) because the intending instantiation 'y' gets captured by the (∀y) quantifier.
It is similar with using instances of the Schema of Abstraction. We don't want any capturing on the instantiations, we need to go careful if the scope or body of the abstraction has quantifiers in it. That is a formal detail that is rarely met in practice.]
To continue, since the Axiom Schema of Abstraction is a schema. when you use it in the software you will be asked what formula you want as the body or 'scope' of it (and you will want any well formed formula with a free x in it).
And now we (ie you) can prove some theorems
1. Fa ∴ a ε{x:Fx}
2. (a∪b)={x: (xεa∨xεb)}, yε(a∪b)∴ (yεa∨yεb) /*Don't worry at the moment what the symbol ∪ means, you just need to know that (a∪b) is a set. */
3. (a∪b)={x: (xεa∨xεb)}, (yεa∨yεb) ∴ yε(a∪b)
You will find the Axioms for Set Theory under the Advanced Menu, and these two proofs involve Abstraction, Instantiation (and sometimes Identity).
Here is a version of the first one
and a version of the second one
It is worthwhile spending some time looking at the pattern of the second and third ones, considered together. We have an abstraction that has a bunch of logic in it, in this case
{x: (xεa∨xεb)}.
Abstractions are terms (ie names), so we can make identities or definitions linking the abstraction with some other piece of notation that appeals to us. In the example (a∪b) appeals to us and we go
(a∪b)={x: (xεa∨xεb)} /*This is an identity statement between names*./
Then we use the Axiom of Abstraction to show that
yε(a∪b)≡yε{x: (xεa∨xεb)} /*This is an equivalence statement between formulas.*/
At this point, you may guess that we could do a similar thing but with different logical statements as the body of the abstraction eg {x: (xεa∧xεb)}, {x: (xεa∧~xεb)} etc. and indeed we will be doing exactly this.
There is another consideration that comes in here. We have built ourselves a set, using abstraction, which has members satisfying a certain condition; but, for all we know, there could be another set with the same members (even satisfying the same condition). Set theory rules this out by deeming that sets with the same members are equal or identical.
Two sets are equal to each other iff (if, and only if,) they have the same members. So
{b,a,c}= {a,b,c}
This principle, generalized, is known as the Axiom of Extensionality (even Naive Set Theory has some axioms!), formally
(∀x)(∀y)((x=y) ≡(∀z)(zεx≡zεy)) Axiom of Extensionality [Long form].
In English this says, 'Allx, Ally' and we are thinking sets here throughout so 'All sets x, All sets y, x=y if, and only if, All (sets) z, z is a member of x if and only if z is a member of y' .
Learning from mathematicians and a convention that they use
If we started to do proofs in Set Theory using this statement of the Axiom of Extensionality what we would find is that the first two steps of the proofs would be Universal Instantiations to take off the outside Universal Quantifiers, say to
(x=y) ≡(∀z)(zεx≡zεy)
and then, at the end of the proof, we would often Universally generalize a couple of times to put quantifiers back on. So, each of our proofs would have extra 'bracketing' quantifier moves which made everything a little longer and more complex without improving the Set Theory 'guts' of the proof.
What mathematician do to avoid this is to state their axioms, and resulting proofs, with free variables and understand those free variables as being universally quantified (which, from a logical point of view, they are). So working mathematicians would state the Axiom of Extensionality as
(x=y) ≡(∀z)(zεx≡zεy)) Axiom of Extensionality [Short, working mathematicians, form].
And they would do their proofs in terms of xs and ys and end up with a theorem perhaps with free xs and ys in it.
We are going to do this!
A question that arises is whether anything is lost here (another question is what happens if you want to work in terms of as and bs not xs and ys). And the answer to these questions is the same. The long form of the Axiom of Extensionality can be proved from the short form (all you do is to Universally Generalize twice on the short form, using y then x as the variables of quantification). If you remember the rule of Universal Generalization, you can generalize providing the variable of generalization is not free in the assumptions of the attempted step. Now, x and y are free in the short form of the Axiom, but that it not an assumption of the step (it is a theorem freely available at any point, which, itself, does not have assumptions). If you want to work in terms of as and bs, first prove the long form of the Axiom of Extensionality (or any other axioms that shortly will be presented) then instantiate what you have to as and bs.
From now on we will work, like mathematicians, with the simpler free variable approach
Onward
(x=y) ≡(∀z)(zεx≡zεy)) Axiom of Extensionality
We could certainly now prove that {b,a,c}= {a,b,c} (to do it, we would probably also need another principle to the effect that
(x ε {a,b,c})⊃((x=a)v(x=b)v(x=c))
and it would take many lines. We will pass on that.
The order of elements within a set is a matter of indifference {b,a,c} is the same set as{a,b,c}.
[Sometimes presentations discuss the possibility of repeat elements in a set (there cannot be any) So
{b,a,c} is the same as {a,b,b,c} /*note the repeat b*/ .
Discussions of this are somewhat obscure. In the field of Artificial Intelligence there is the notion of a 'bag' and conceptually this comes from 'bag of shopping'; in a bag of shopping you might have 3 (identical) bars of soap, and 2 (identical) cans of beans, making a bag of five items. In Set Theory you cannot really do this, or, at least, not in the same way, the set {soap,soap,soap,beans,beans} contains just 2 elements because there cannot be repeat elements. We can all get confused at this point. Those identical bars of soap are not really identical. Suffice it to say, do not write anything like {a,b,b,c} in Set Theory because no one will understand it-- it seems to be a four element set with just three member. Just avoid.]
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.