George: User Manual

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 (capital i)	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

We can also use natural deduction to prove two terms describing sets are equal by using transformations of the terms themselves. Implicitly, this method is using the ND rule eq_e and the set theory axioms/derived rules. For example:

#check ND

|- univ diff (B inter univ) = compl(B)

1) univ diff (B inter univ) = univ diff B    by set // universal set identities
2) univ diff (B inter univ) = compl(B) by set on 1 // universal set identities on 1

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 
8) x in compl(B) union compl(C)  by set // union

What does george check?

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.

george: User Manual

Set Theory

What does george check?