[
Introduction
]
[
File Structure
]
[
#check PROP
]
[
#check PRED
]
[
#check PREDTYPES
]
[
#check TP
]
[
#check ND
]
[
#check ST
]
[
Arithmetic
]
[
Sets
]
[
#check Z
]
[
#check PC
]
[
Contributions by Students
]
[
Credits
]
Keywords
]
Set theory is a theory of predicate logic in which the functions and predicates of operations on sets can be used in predicate logic expressions and proofs. Below is the syntax for these operators, many of which are infix operators. These can be used in any predicate logic formula.
| Syntax in george | Meaning | Syntax in george | Meaning |
|---|---|---|---|
| { 1,2,4} | set enumeration | { f(x,y) for x: S, y:Q if P(x,y) } | set comprehension |
| dom(R) | domain of R | ||
| empty | empty set | ran(R) | range of R |
| univ | universal set | R~ | inverse of R |
| x in B | set membership | id(P) | identity relation of set P |
| B sube C | sube | iter(R,n) | iteration of R n times |
| B sub C | proper subset | S <| R | domain restriction of R to S |
| pow(B) | power set of B | S <-| R | domain subtraction of R to S | B union C | union of B and C | R |> S | range restriction of R to S |
| B inter C | intersection of B and C | R |-> S | range subtraction of R to S |
| compl(B) | absolute complement of B | R (+) S | relational override |
| P diff Q | difference | R (|S|) | relational image |
| card(B) | size of B | R ; S | relational composition |
| gen_U(B) | generalized union of B | gen_I(B) | generalized intersection of B |
| B prod C | cartesian product of B and C |
Rather than trying to define and remember precedence and associativity for all these operations, please use brackets.
Here is an example of a response to a question that requires a formalization in set theory:
#check PRED // Cars that drive fast are dangerous. (Cars inter Fast) sube Dangerous #check PRED // Cars, which drive fast, are dangerous. (Cars sube Fast) & (Cars sube Dangerous)
We can do proofs about sets using both natural deduction and transformational proof. There are several different styles of proof, which we illustrate below.
In natural deduction, we use the additional rule by set on ... as the justification for proof lines that rely on the axioms/derived rules of set theory. The derived rules of set theory can also be used. (See the set theory summary page for the list of axioms and derived rules of set theory.)
Here is an example of the response to a question that requires a natural deduction proof about sets:
#check ND
|- empty sube B
1) for every xg {
2) assume xg in empty {
3) !(xg in empty) by set // empty set
4) xg in B by not_e on 2,3
}
5) xg in empty => xg in B by imp_i on 2-4
}
6) forall x. x in empty => x in B by forall_i on 1-5
7) empty sube B by set on 6 // subset
There are two different styles of transformational proof that we use regularly for proofs about sets. The first method is to prove <-> as we have done before with the additional TP rule of by set // ... where "..." is replaced by an axiom/derived rule of set theory from the summary page. No line is needed because in TP we are always referring to the previous line. For example:
#check TP B = C <-> B sube C & C sube B 1) B = C 2) forall x. x in B <=> x in C by set // equality 3) forall x. (x in B => x in C) & (x in C => x in B) by equiv 4) (forall x. x in B => x in C) & (forall x. x in C => x in B) by forall_over_and 5) (B sube C) & (forall x. x in C => x in B) by set // subset 6) (B sube C) & (C sube B) by set // subset
The second method is to prove two terms describing sets are equal by showing an element is in one set iff it is in the other set. For example:
#check TP // to prove compl(B inter C) = compl(B) union compl(C) // we show x in compl(B inter C) <-> x in (compl(B) union compl(C)) 1) x in compl(B inter C) 2) x in univ & !(x in B inter C) by set // abs compl 3) x in univ & !(x in B & x in C) by set // intersection 4) x in univ & (!(x in B) | !(x in C)) by dm 5) x in univ & !(x in B) | (x in univ) & !(x in C) by distr 6) x in compl(B) | (x in univ) & !(x in C) by set // abs compl 7) x in compl(B) | x in compl(C) by set // abs compl
george treats the "by set" rules as magic rules and does not check the correctness of these, therefore george gives you a warning that these rules have been used and not checked, but for the other rules, it checks that they have been used correctly.