Set Theory For Computer Science - University Of Cambridge
Set Theory for Computer ScienceGlynn Winskelgw104@cl.cam.ac.ukc 2010 Glynn WinskelOctober 11, 2010
2Syllabus Mathematical argument: Basic mathematical notation and argument, including proof by contradiction, mathematical induction and its variants. Sets and logic: Subsets of a fixed set as a Boolean algebra. Venn diagrams.Propositional 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 relation.Equivalence relations and partitions. Directed graphs and partial orders.Size of sets, especially countability. Cantor’s diagonal argument to showthe reals are uncountable. Constructions on sets: Russell’s paradox. Basic sets, comprehension, indexed sets, unions, intersections, products, disjoint unions, powersets.Characteristic functions. Sets of functions. Lambda notation for functions. Cantor’s diagonal argument to show powerset strictly increases size.An 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 induction. Examples. Constructing well-founded relations, including productand lexicographic product of well-founded relations. Applications. Wellfounded recursion. Inductively-defined properties and classes: Ordinals and transfinite induction. Fraenkel-Mostowski sets: Failure of the axiom of choice in Fraenkel-Mostowskisets. Freshness. Nominal sets.Aims 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 techniques.
3 understand the formalization of basic logic (validity, entailment and truth)in set theory. define sets inductively using rules, formulate corresponding proof principles, and prove properties about inductively-defined sets. understand Tarski’s fixed point theorem and the proof principles associated 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 properties.A 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.)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 mortal.But 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, viz. the set of all men. It was this objectification of meaning, understanding 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 different forms of infinity and, almost incidentally, to shortcut several traditionalmathematical arguments.But the power of sets came at a price; it came with dangerous paradoxes.The work of Boole and others suggested a programme exposited by Frege, andRussell and Whitehead, to build a foundation for all of Mathematics on Logic.Though to be more accurate, they were really reinventing Logic in the process,and regarding it as intimately bound up with a theory of sets. 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 and
4Whitehead’s theory of stratified types and then more elegantly, in for example the influential work of Zermelo and Fraenkel. The notion of set is now acornerstone of Mathematics.The precise notion of proof present in the work of Russell and Whitehead laidthe scene for Gödel’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 prove all the statements within the system which are true. Gödel’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ödel himself, Church, Turing and others, it was realised by the mid1930’s that Gödel’s incompleteness result rested on a fundamental notion, thatof computability. Arguably this marks the birth of Computer Science.MotivationWhy 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 Theory.Why is Set Theory important for Computer Science? It’s a useful tool forformalising and reasoning about computation and the objects of computation.Set Theory is indivisible from Logic where Computer Science has its roots.It 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 Theory.The 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. Set Theory is likely to be aroundlong after most present-day programming languages have faded from memory.A 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 meet.The 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. This course is not about 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 peripherally.In 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. Constructing
5proofs in mathematics is similar. Often a tolerant openness and awareness is important 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. 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 assumptions and the goal. Often starting to write down a proof helps you discoverit. You may have already experienced this in carrying out proofs by induction.It 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 it.Of 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. For this reason you are encouraged to do theexercises—most of them are placed strategically in the appropriate place in thetext.Additional reading: The notes are self-contained. The more set-theory oriented books below are those of Devlin, Nissanke and Stanat-McAllister. Onlinesources such as Wikipedia can also be helpful.Devlin, K. (2003) Sets, Functions, and Logic, An Introduction to Abstract Mathematics. Chapman & Hall/CRC Mathematics (3rd ed.).Biggs, N.L. (1989). Discrete mathematics. Oxford University Press.Mattson, H.F. Jr (1993). Discrete mathematics. Wiley.Nissanke, N. (1999). Introductory logic and sets for computer scientists. AddisonWesley.Pólya, G. (1980). How to solve it. Penguin.Stanat, D.F., and McAllister, D.F. (1977), Discrete Mathematics in ComputerScience.Prentice-Hall.Acknowledgements: To Hasan Amjad, Katy Edgcombe, Marcelo Fiore, ThomasForster, Ian Grant, Martin Hyland, Frank King, Ken Moody, Alan Mycroft,Andy Pitts, Peter Robinson, Sam Staton, Dave Turner for helpful suggestions.
6
Contents1 Mathematical argument1.1 Logical notation . . . . . . .1.2 Patterns of proof . . . . . . .1.2.1 Chains of implications1.2.2 Proof by contradiction1.2.3 Argument by cases . .1.2.4 Existential properties1.2.5 Universal properties .1.3 Mathematical induction . . .1111131313141515152 Sets and Logic2.1 Sets . . . . . . . . . . . . . . . . . . .2.2 Set laws . . . . . . . . . . . . . . . . .2.2.1 The Boolean algebra of sets . .2.2.2 Venn diagrams . . . . . . . . .2.2.3 Boolean algebra and properties2.3 Propositional logic . . . . . . . . . . .2.3.1 Boolean propositions . . . . . .2.3.2 Models . . . . . . . . . . . . .2.3.3 Truth assignments . . . . . . .2.3.4 Truth tables . . . . . . . . . . .2.3.5 Methods . . . . . . . . . . . . .2525262630323232343740423 Relations and functions3.1 Ordered pairs and products . . . . . . . . . . . .3.2 Relations and functions . . . . . . . . . . . . . .3.2.1 Composing relations and functions . . . .3.2.2 Direct and inverse image under a relation3.3 Relations as structure . . . . . . . . . . . . . . .3.3.1 Directed graphs . . . . . . . . . . . . . . .3.3.2 Equivalence relations . . . . . . . . . . . .3.3.3 Partial orders . . . . . . . . . . . . . . . .3.4 Size of sets . . . . . . . . . . . . . . . . . . . . .3.4.1 Countability . . . . . . . . . . . . . . . .4545464749505050535555.7.
8CONTENTS3.4.2Uncountability . . . . . . . . . . . . . . . . . . . . . . . .4 Constructions on sets4.1 Russell’s paradox . . . . . . .4.2 Constructing sets . . . . . . .4.2.1 Basic sets . . . . . . .4.2.2 Constructions . . . . .4.2.3 Axioms of set theory .4.3 Some consequences . . . . . .4.3.1 Sets of functions . . .4.3.2 Sets of unlimited size .59.6363646464686969715 Inductive definitions5.1 Sets defined by rules—examples . . . .5.2 Inductively-defined sets . . . . . . . .5.3 Rule induction . . . . . . . . . . . . .5.3.1 Transitive closure of a relation5.4 Derivation trees . . . . . . . . . . . . .5.5 Least fixed points . . . . . . . . . . . .5.6 Tarski’s fixed point theorem . . . . . .73737778828386886 Well-founded induction6.1 Well-founded relations . . . . . . . . . . . .6.2 Well-founded induction . . . . . . . . . . . .6.3 Building well-founded relations . . . . . . .6.3.1 Fundamental well-founded relations6.3.2 Transitive closure . . . . . . . . . . .6.3.3 Product . . . . . . . . . . . . . . . .6.3.4 Lexicographic products . . . . . . .6.3.5 Inverse image . . . . . . . . . . . . .6.4 Applications . . . . . . . . . . . . . . . . . .6.4.1 Euclid’s algorithm for hcf . . . . . .6.4.2 Eulerian graphs . . . . . . . . . . . .6.4.3 Ackermann’s function . . . . . . . .6.5 Well-founded recursion . . . . . . . . . . . .6.5.1 The proof of well-founded recursion.91. 91. 92. 94. 94. 94. 94. 95. 96. 96. 96. 98. 99. 101. 1037 Inductively-defined classes7.1 Sets, properties and classes . . . . . . . . . . . . .7.2 Inductively-defined properties and classes . . . . .7.3 Induction principles for inductively-defined classes7.4 Ordinals . . . . . . . . . . . . . . . . . . . . . . . .7.4.1 Properties of ordinals . . . . . . . . . . . .7.4.2 The Burali-Forti paradox . . . . . . . . . .7.4.3 Transfinite induction and recursion . . . . .7.4.4 Cardinals as ordinals . . . . . . . . . . . . .105105106107107109110111112
CONTENTS7.57.4.5 Tarski’s fixed point theorem revisited . . . . . . . . . . . 113The cumulative hierarchy . . . . . . . . . . . . . . . . . . . . . . 1158 Fraenkel-Mostowski sets8.1 Atoms and permutations . . . . . . . . . . . . . .8.2 Classes with an action . . . . . . . . . . . . . . .8.3 Fraenkel-Mostowski sets . . . . . . . . . . . . . .8.4 Constructions on FM sets . . . . . . . . . . . . .8.4.1 Failure of the axiom of choice in FM sets8.5 Freshness . . . . . . . . . . . . . . . . . . . . . .8.6 Nominal sets . . . . . . . . . . . . . . . . . . . .8.6.1 Nominal sets and equivariant functions . .8.6.2 α-equivalence and atom abstraction . . .99Exercises.117117118119121122122126126127131
10CONTENTS
Chapter 1Mathematical argumentBasic mathematical notation and methods of argument are introduced, including a review of the important principle of mathematical induction.1.1Logical notationWe shall use some informal logical notation in order to stop our mathematicalstatements getting out of hand. For statements (or assertions) A and B, weshall commonly use abbreviations like: A & B for (A and B), the conjunction of A and B, A B for (A implies B), which means (if A then B), and so is automatically true when A is false, A B to mean (A iff B), which abbreviates (A if and only if B), andexpresses the logical equivalence of A and B.We shall also make statements by forming disjunctions (A or B), with the selfevident meaning, and negations (not A), sometimes written A, which is trueiff A is false. There is a tradition to write for instance 7 6 5 instead of (7 5),which reflects what we generally say: “7 is not less than 5” rather than “not 7is less than 5.”The statements may contain variables (or unknowns, or place-holders), as in(x 3) & (y 7)which is true when the variables x and y over integers stand for integers less thanor equal to 3 and 7 respectively, and false otherwise. A statement like P (x, y),which involves variables x, y, is called a predicate (or property, or relation,or condition) and it only becomes true or false when the pair x, y stand forparticular things.11
12CHAPTER 1. MATHEMATICAL ARGUMENTWe use logical quantifiers , read “there exists”, and , read “ for all”. Thenyou can read assertions like x. P (x)as abbreviating “for some x, P (x)” or “there exists x such that P (x)”, and x. P (x)as abbreviating “ for all x, P (x)” or “for any x, P (x)”. The statement x, y, · · · , z. P (x, y, · · · , z)abbreviates x y · · · z. P (x, y, · · · , z),and x, y, · · · , z. P (x, y, · · · , z)abbreviates x y · · · z. P (x, y, · · · , z).Sometimes you’ll see a range for the quantification given explicitly as in x (0 x k). P (x). Later, we often wish to specify a set X over whicha quantified variable ranges. Then one writes x X. P (x)—read “for all xin X, P (x)”— instead of x. x X P (x), and x X. P (x) instead of x. x X & P (x).There is another useful notation associated with quantifiers. Occasionallyone wants to say not just that there exists some x satisfying a property P (x)but also that x is the unique object satisfying P (x). It is traditional to write !x. P (x)as an abbreviation for( x. P (x)) & ( y, z. P (y) & P (z) y z)which means that there is some x satisfying the property P (x) and also thatif any y, z both satisfy the property they are equal. This expresses that thereexists a unique x satisfying P (x).Occasionally, and largely for abbreviation, we will write e.g., X def Eto mean that X is defined to be E. Similarly, we will sometimes use e.g.,P (x) def A in defining a property in terms of an expression A.Exercise 1.1 What is the difference between x.( y.P (x, y)) and y.( x.P (x, y))?[You might like to consider P (x, y) to mean “x loves y.”]2
1.2. PATTERNS OF PROOF1.213Patterns of proofThere is no magic formula for discovering proofs in anything but the simplestcontexts. However often the initial understanding of a problem suggests a general pattern of proof. Patterns of proof like those below appear frequently, oftenlocally as ingredients of a bigger proof, and are often amongst the first thingsto try. It is perhaps best to tackle this section fairly quickly at a first reading,and revisit it later when you have had more experience in doing proofs.1.2.1Chains of implicationsTo prove an A B it suffices to show that starting from the assumption A onecan prove B. Often a proof of A B factors into a chain of implications, eachone a manageable step:A A1 ··· An B .This really stands forA A1 , A1 A2 , · · · , An B .One can just as well write “Therefore” (or “ ”) between the different lines, andthis is preferable if the assertions A1 , · · · , An are large.A logical equivalence A B stands for both A B and B A. Oneoften sees a proof of a logical equivalence A B broken down into a chainA A1 · · · An B .A common mistake is not to check the equivalence in the backwards direction, sothat while the implication Ai 1 to Ai is obvious enough, the reverse implicationfrom Ai to Ai 1 is unclear, in which case an explanation is needed, or evenuntrue. Remember, while a proof of A B very often does factor into aproof of A B and B A, the proof route taken in showing B A needn’tbe the reverse of that t
Computer Science from theory to practice; Computer Science, being a science of the arti cial, has had many of its constructs and ideas inspired by Set Theory. The strong tradition, universality and neutrality of Set Theory make it rm common ground on which to provide uni cation between seemingly disparate areas and notations of Computer Science.
Bruksanvisning för bilstereo . Bruksanvisning for bilstereo . Instrukcja obsługi samochodowego odtwarzacza stereo . Operating Instructions for Car Stereo . 610-104 . SV . Bruksanvisning i original
10 tips och tricks för att lyckas med ert sap-projekt 20 SAPSANYTT 2/2015 De flesta projektledare känner säkert till Cobb’s paradox. Martin Cobb verkade som CIO för sekretariatet för Treasury Board of Canada 1995 då han ställde frågan
service i Norge och Finland drivs inom ramen för ett enskilt företag (NRK. 1 och Yleisradio), fin ns det i Sverige tre: Ett för tv (Sveriges Television , SVT ), ett för radio (Sveriges Radio , SR ) och ett för utbildnings program (Sveriges Utbildningsradio, UR, vilket till följd av sin begränsade storlek inte återfinns bland de 25 största
Hotell För hotell anges de tre klasserna A/B, C och D. Det betyder att den "normala" standarden C är acceptabel men att motiven för en högre standard är starka. Ljudklass C motsvarar de tidigare normkraven för hotell, ljudklass A/B motsvarar kraven för moderna hotell med hög standard och ljudklass D kan användas vid
LÄS NOGGRANT FÖLJANDE VILLKOR FÖR APPLE DEVELOPER PROGRAM LICENCE . Apple Developer Program License Agreement Syfte Du vill använda Apple-mjukvara (enligt definitionen nedan) för att utveckla en eller flera Applikationer (enligt definitionen nedan) för Apple-märkta produkter. . Applikationer som utvecklas för iOS-produkter, Apple .
och krav. Maskinerna skriver ut upp till fyra tum breda etiketter med direkt termoteknik och termotransferteknik och är lämpliga för en lång rad användningsområden på vertikala marknader. TD-seriens professionella etikettskrivare för . skrivbordet. Brothers nya avancerade 4-tums etikettskrivare för skrivbordet är effektiva och enkla att
Den kanadensiska språkvetaren Jim Cummins har visat i sin forskning från år 1979 att det kan ta 1 till 3 år för att lära sig ett vardagsspråk och mellan 5 till 7 år för att behärska ett akademiskt språk.4 Han införde två begrepp för att beskriva elevernas språkliga kompetens: BI
language of instruction was a common problem identified by many. Based on this issue a research investigation with the aim of raising teacher awareness of the strategies and techniques that could be used to support the language development of young learners was conducted. The Research Investigation . In 2010, a research project funded by a grant from the Jeff Thompson Award, was conducted to .
