Set Theory for Computer Science - University of Cambridge

1 Set Theory for Computer ScienceGlynn 2010 Glynn WinskelOctober 11, 20102 Syllabus Mathematical argument:Basic mathematical notation and argument, in-cluding proof by contradiction, mathematical induction and its variants. Sets and logic:Subsets of a fixed set as a Boolean algebra. Venn logic and its models. Validity, entailment, and equivalence ofboolean propositions. Truth tables. Structural induction. Simplificationof boolean propositions and set expressions. Relations and functions:Product of sets. Relations, functions and partialfunctions. Composition and identity relations. Injective, surjective andbijective functions. Direct and inverse image of a set under a relations and partitions. Directed graphs and partial of sets, especially countability. Cantor s diagonal argument to showthe reals are uncountable.

2 Constructions on sets:Russell s paradox. Basic sets, comprehension, in-dexed sets, unions, intersections, products, disjoint unions, functions. Sets of functions. Lambda notation for func-tions. Cantor s diagonal argument to show powerset strictly increases informal presentation of the axioms of Zermelo-Fraenkel set Theory andthe axiom of choice. Inductive definitions:Using rules to define sets. Reasoning principles:rule induction and its instances; induction on derivations. Applications,including transitive closure of a relation. Inductive definitions as leastfixed points. Tarski s fixed point theorem for monotonic functions on apowerset. Maximum fixed points and coinduction. Well-founded induction:Well-founded relations and well-founded induc-tion.

3 Examples. Constructing well-founded relations, including productand lexicographic product of well-founded relations. Applications. Well-founded recursion. Inductively-defined properties and classes:Ordinals and transfinite induc-tion. Fraenkel-Mostowski sets:Failure of the axiom of choice in Fraenkel-Mostowskisets. Freshness. Nominal and objectivesThe aim is to introduce fundamental concepts and techniques in set Theory inpreparation for its many applications in Computer Science . On completing thiscourse, students should be able to understand and be able to use the language of set Theory ; prove anddisprove assertions using a variety of understand the formalization of basic logic (validity, entailment and truth)in set Theory . define sets inductively using rules, formulate corresponding proof princi-ples, and prove properties about inductively-defined sets.

4 Understand Tarski s fixed point theorem and the proof principles associ-ated with the least and greatest fixed points of monotonic functions on apowerset. understand and apply the principle of well-founded induction, includingtransfinite induction on the ordinals. have a basic understanding of Fraenkel-Mostowski sets and their brief history of setsA set is an unordered collection of objects, and as such a set is determined bythe objects it contains. Before the 19th century it was uncommon to think ofsets as completed objects in their own right. Mathematicians were familiar withproperties such as being a natural number, or being irrational, but it was rare tothink of say the collection of rational numbers as itself an object. (There wereexceptions. From Euclid mathematicians were used to thinking of geometricobjects such as lines and planes and spheres which we might today identifywith their sets of points.)

5 In the mid 19th century there was a renaissance in Logic. For thousandsof years, since the time of Aristotle and before, learned individuals had beenfamiliar with syllogisms as patterns of legitimate reasoning, for example:All men are mortal. Socrates is a man. Therefore Socrates is syllogisms involved descriptions of properties. The idea of pioneers such asBoole was to assign a meaning as a set to these descriptions. For example, thetwo descriptions is a man and is a male homo sapiens both describe thesame set, set of all men. It was this objectification of meaning, under-standing properties as sets, that led to a rebirth of Logic and Mathematics inthe 19th century. Cantor took the idea of set to a revolutionary level, unveilingits true power. By inventing a notion of size of set he was able compare dif-ferent forms of infinity and, almost incidentally, to shortcut several traditionalmathematical the power of sets came at a price; it came with dangerous work of Boole and others suggested a programme exposited by Frege, andRussell and Whitehead, to build a foundation for all of Mathematics on to be more accurate, they were really reinventing Logic in the process,and regarding it as intimately bound up with a Theory of sets.

6 The paradoxesof set Theory were a real threat to the security of the foundations. But witha lot of worry and care the paradoxes were sidestepped, first by Russell and4 Whitehead s Theory of stratified types and then more elegantly, in for exam-ple the influential work of Zermelo and Fraenkel. The notion of set is now acornerstone of precise notion of proof present in the work of Russell and Whitehead laidthe scene for G odel s astounding result of 1931: any sound proof system able todeal with arithmetic will necessarily be incomplete, in the sense that it will beimpossible to proveallthe statements within the system which are true. G odel stheorem relied on the mechanical nature of proof in order to be able to encodeproofs back into the proof system itself. After a flurry of activity, through thework of G odel himself, Church, Turing and others, it was realised by the mid1930 s that G odel s incompleteness result rested on a fundamental notion, thatof computability.

7 Arguably this marks the birth of Computer learn Set Theory ? Set Theory is an important language and tool forreasoning. It s a basis for Mathematics pretty much all Mathematics can beformalised in Set is Set Theory important for Computer Science ? It s a useful tool forformalising and reasoning about computation and the objects of Theory is indivisible from Logic where Computer Science has its has been and is likely to continue to be a a source of fundamental ideas inComputer Science from Theory to practice; Computer Science , being a Science ofthe artificial, has had many of its constructs and ideas inspired by Set strong tradition, universality and neutrality of Set Theory make it firmcommon ground on which to provide unification between seemingly disparateareas and notations of Computer Science .

8 Set Theory is likely to be aroundlong after most present-day programming languages have faded from knowledge of Set Theory should facilitate your ability to think abstractly. Itwill provide you with a foundation on which to build a firm understanding andanalysis of the new ideas in Computer Science that you will art of proofProof is the activity of discovering and confirming truth. Proofs in mathematicsare not so far removed from coherent logical arguments of an everyday kind, ofthe sort a straight-thinking lawyer or politician might apply an Obama, nota Bush! A main aim of this course and its attendant seminars is to help youharness that everyday facility to write down proofs which communicate well toother people. Here there s an art in getting the balance right: too much detailand you can t see the wood for the trees; too little and it s hard to fill in thegaps.

9 This course isnotabout teaching you how to do very formal proofs withina formal logical system, of the kind acceptable to machine verification that san important topic in itself, and one which we will touch on Italy it s said that it requires two people to make a good salad dressing;a generous person to add the oil and a mean person the vinegar. Constructing5proofs in mathematics is similar. Often a tolerant openness and awareness is im-portant in discovering or understanding a proof, while a strictness and disciplineis needed in writing it down. There are many different styles of thinking, evenamongst professional mathematicians, yet they can communicate well throughthe common medium of written proof. It s important not to confuse the rigourof a well-written-down proof with the human and very individual activity ofgoing about discovering it or understanding it.

10 Too much of a straightjacket onyour thinking is likely to stymie anything but the simplest proofs. On the otherhand too little discipline, and writing down too little on the way to a proof, canleave you uncertain and lost. When you cannot see a proof immediately (thismay happen most of the time initially), it can help to write down the assump-tions and the goal. Often starting to write down a proof helps you discoverit. You may have already experienced this in carrying out proofs by can happen that the induction hypothesis one starts out with isn t strongenough to get the induction step. But starting to do the proof even with the wrong induction hypothesis can help you spot how to strengthen course, there s no better way to learn the art of proof than by doing proofs,no better way to read and understand a proof than to pause occasionally andtry to continue the proof yourself.