New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

Be part of our community, it's free to join!

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here


by: Beatriz Mitchell

LOGIC FOR COMPUTER SCIENCE CS 201 intro into computer science

Beatriz Mitchell
GPA 4.0

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

CS 201 intro into computer science
Mr. Burns
Class Notes
25 ?




Popular in CS 201 intro into computer science

Popular in ComputerScienence

This 311 page Class Notes was uploaded by Beatriz Mitchell on Monday November 2, 2015. The Class Notes belongs to CS 201 intro into computer science at University of New Mexico taught by Mr. Burns in Fall 2015. Since its upload, it has received 25 views. For similar materials see CS 201 intro into computer science in ComputerScienence at University of New Mexico.

Similar to CS 201 intro into computer science at UNM

Popular in ComputerScienence




Report this Material


What is Karma?


Karma is the currency of StudySoup.

You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 11/02/15
LOGIC FOR COMPUTER SCIENCE Steve Reeves and Mike Clarke Queen Mary and Westfield College University of London U.K. Department of Computer Science UnNew Zealand Waikato ©1990 and 2003 The programs in this book have been included for their instructional value. They have been tested with care but are not guaranteed for any particular purpose. The authors and publishers do not offer any warranties or representations, nor do they accept any liabilities with respect to the programs. The contents of this book were first published in 1990 by Addison-Wesley Publishers Ltd. Preface to 1990 edition Aims The aim of this book is to give students of computer science a working knowledge of the relevant parts of logic. It is not intended to be a review of applications of logic in computer science, neither is it primarily intended to be a first course in logic for students of mathematics or philosophy, although we believe that mush of the material will be increasingly relevant to both of these groups as computational ideas pervade their syllabuses. Most controversial perhaps will be our decision to include modal and intuitionistic logic in an introductory text, the inevitably cost being a rather more summary treatment of some aspects of classical predicate logic. We believe, however, that a glance at the wide variety of ways in which logic is used in computer science fully justifies this approach. Certainly classical predicate logic is the basic tool of sequential program verification, but modal and temporal logics are increasingly being used for distributed and concurrent systems and intuitionistic logic provides a basis for expressing specifications and deriving programs. Horn clause logic and resolution underlie the very widespread use of logic programming, while algorithms for automated theorem proving have long been of interest to computer scientists for both their intrinsic interest and the applications in artificial intelligence. One major (and deliberate) omission is the standard development of the logical basis of set theory and arithmetic. These theories are so well covered in a number of excellent and widely available texts (many of which are referenced in the text or are among the sources we acknowledge at the end of this preface) that we preferred to use the space for less well-exposed topics. Of course, the need to formalize arithmetic and set theory has led to major developments in logic and computer science and we have tried to give the historical perspective, while referring readers elsewhere for the detail. iii iv Different disciplines have different motivations for studying logic and correspondingly different conventions of notation and rigour. To keep the within reasonable bounds we have decided to omit some of the lengthier explanations and proofs found in traditional logic texts in favour of introducing topics considered more ‘advanced’, that are central to modern computer science. In many cases, where proof methods have been specified by non-deterministic sets of rules, we have been more precise than usual by giving algorithms and programs; in other cases we have relied on the background of our students to keep routine formal development to a minimum. Another major departure is that we present many of the definitions and algorithms as computer programs in, not just one but, two programming languages. We have chosen Prolog and SML, partly because they are both highly succinct and suitable languages for the procedures we want to express, but also because they have their roots, respectively in logic and the l–calculus, two of the most important theoretical developments that underlie computer science and the theory of computability. Either of the languages is sufficient, but a student who carefully studies the programs in both languages will learn a lot about the theory and technique of declarative programming as well as about the logical definitions and algorithms that the programs express. In Appendix A we give a brief introduction to the philosophy and facilities of both languages, but this is aimed to some extent at teachers and students with a considerable background in computer science. The less sophisticated will need access to one or other of the introductory texts that we recommend. That being said, the programs are designed to be readable ad should relay some message even to non- programmers, perhaps helping them to realize that much of logic is inseparable from the notion of an effective algorithm, and even encourage them to start programming. Overall, our aim has been to show how computer science and logic are closely linked. We hope that students will see that what they might have considered a dry subject without obvious applications is being put to good use and vigorously developed by computer scientists. Readership Much of the material has been tested in a course given to first-year undergraduate students in computer science who, at that stage, have had an introductory course in discrete mathematics and a first programming course that emphasizes recursion, inductive proof and scope of definition. So they already have a fair grasp at a semiformal level of notions such as set, function, relation, formal v language, free and bounds variable and mathematical induction, and we believe that such a background will, if not already standard, soon become so for first-year students of computer science. The students, we are glad to say, bear out our conviction that an introductory logic course can successfully go beyond what is usually considered tot he be the appropriate level. They are able to actually do proofs using the methods we teach and are surprised and challenged by the idea of several logics. We feel that this is because computer science, properly taught, makes the student of logic easier, and vice versa. The activity of constructing and reasoning about programs in not all that different from the activity of constructing and reasoning about proofs. Acknowledgements Our colleagues, also, have made a big contribution to the development of the course, and subsequently the book. We would single out for special mention, in no particular order, Peter Burton, Wilfrid Hodges, Doug Goldson, Peter Landin, Sarah Lloyd-Jones, Mike Hopkins, Keith Clarke, Richard Bornat, Steve Sommerville, Dave Saunders, Mel Slater, John Bell and Mark Christian, and well as those further away—Alan Bundy, Dov Gabbay—who have influenced our views on the more advanced topics. Finally, it will be obvious that we have been strongly influenced, and greatly helped, by many other texts whose development fo the subject we have studied, and in many instances borrowed. These have included Hodges (1977), Logic, Hamilton (1978), Logic for Mathematicians, Boolos and Jeffrey (1980), Computability and Logic, Scott et al. (1981), Foundations of Logic Programming , and Martin-Löf (1985), Constructive Mathematics and Computer Programming. Steve Reeves Mike Clarke QMW, University of London November, 1989 Preface to 2003 edition Since 1990 much has changed in our subject and many further chapters could be added to the book Mike and I wrote in 1989-1990. However, I think it is good to be able to say that all of the things we wrote about then are still relevant and being used in many areas of computer science today, which is something not many authors iv of computer science texts looking back over 13 years from 2003 could say—we clearly chose well. However, there are two reasons why the book has not changed. One is that no company, today, thinks it worth publishing (well, not Addison-Wesley anyhow—now part of Pearson). To some extent you can’t blame them—computer science has become more and more a ticket to a good job rather than an intellectual undertaking (that is likely to lead to a good job) taught and studied by people who are interested in it. (many of our current students are not interested in the subject, or are not very good at it, so I hate to think what their working lives, in terms of self-fulfillment, are going to be like). The publishers look around at all the courses which teach short-term skills rather than lasting knowledge and see that logic has little place, and see that a book on logic for computer science does not represent an opportunity to make monetary profits. Why, then, has the book re-appeared? Because of repeated demands from around the world (but mainly from the USA) for copies of it! There are no longer any (new) copies for sale, so given the demand something had to be done. Hence this ersatz edition. It’s not as high quality as AW’s was, but then I’m not a type-setter, printer, bookbinder, designer etc. It was produced from the original Word files we gave to AW (from which, after much re-typing and re-design, they produced the 1990 edition). Those files were written using a couple of Macintosh SEs. The files have traveled around the world with me, moving from computer to computer until the 2003 version has been produced on an eMac and a Titanium Powerbook. There is one constant in Word—it still crashes reliably about once a day! The other reason the book has not been re-written is that Mike Clarke died in 1994, so the version before you stands as a memorial to him—he was a friend and a mentor, and you can’t be more than that. Steve Reeves University of Waikato January 2003 CONTENTS Preface to 1990 edition iii Preface to 2003 edition v CONTENTS vii Introduction 1 1.1. Aims and Objectives 1 1.2. Background history 2 1.3. Background terminology 2 1.4. Propositions, Beliefs and Declarative Sentences 5 1.5. Contradictions 6 1.6. Formalization 7 vii viii Formalizing the Language 9 2.1 Informal Propositional Calculus 9 2.2 Arguments 20 2.3 Functional Completeness 27 2.4 Consistency, Inconsistency, Entailment. 28 2.5 Formal Propositional Calculus 33 2.6 Soundness and Completeness for propositional calculus 42 Extending the language 49 3.1. Informal predicate calculus 49 3.2. FDS for predicate calculus 60 3.3. Historical discussion 65 3.4. Models and Theories 68 Semantic Tableaux 71 4.1. Introduction 71 4.2. Semantic Tableaux for Propositional Calculus 72 4.3. Soundness and Completeness for Propositional Calculus 80 4.4. Semantic Tableaux for Predicate Calculus 89 4.5. Soundness and Completeness for Predicate Calculus 92 Natural Deduction 99 5.1. Rules and Proofs 99 5.2. The Sequent Calculus 110 5.3. Generalizing the logic 117 5.4. What is Logic Ultimately? 121 ix Some Extended Examples 125 6.1. Introduction 125 6.2. Theory examples 125 6.3. Gödel and the limits of formalization 144 Logic Programming 147 7.1. Introduction 147 7.2. Substitution and Unification 153 7.3. Resolution 159 7.4. Least Herbrand models and a declarative semantics for definite clause programs 162 Non-Standard Logics 167 8.1. Introduction 167 8.2. Necessity and Possibility 167 8.3. Possible world semantics 169 8.4. Frames, interpretations and models 170 8.5. Truth-functionality and modal logic 174 8.6. Systems of modal logic 175 8.7. A tableau system for S4 175 8.8. One use for modal logic in programming 184 8.9. Tableaux for Intuitionistic Logic 186 Further Study 193 9.1. Introduction 193 9.2. Connection method 193 9.3. LCF 197 9.4. Temporal and dynamic logics 204 9.5. Intuitionistic logic 210 x Introductions to Standard ML and Prolog 221 A.1. Introduction 221 A.2. Standard ML 221 A.3. Prolog 239 Programs in Standard ML and Prolog 255 B.1.Programs in SML 255 B.2. Programs in Prolog 279 Solutions to Selected Exercises 281 REFERENCES 293 INDEX 297 CHAPTER ONE Introduction 1.1. Aims and Objectives This book will differ from most others with similar titles because we aim to give you not one or two ways of looking at Logic, but many. The forms of reasoning that are fundamental to Computer Science are not necessarily those most familiar from a study of Mathematics and this gives us the opportunity to develop the subject along two dimensions, looking not only at different methods for implementing one particular mode of reasoning, but also at different ways of formalizing the process of reasoning itself. There are many reasons why a computer scientist should need to study logic. Not only has it historically formed the roots of computer science, both Church's and Turing's work being motivated by the decision problem for first-order logic, but nowadays we are finding conversely that computer science is generating an explosion of interest in logic, with the desire to automate reasoning and the necessity to prove programs correct. Basically, logic is about formalizing language and reasoning, and computer science addresses similar problems with the extra task, having formalized them, of expressing those formalizations, in the technical sense of producing mechanisms which follow the rules that they lay down. This, indeed, has led to the recent use of computer science for investigating logics in an experimental way, exploring some of them much more thoroughly than was possible when the 'computer' was a person rather than a machine. 1 2 INTRODUCTION What we hope then to show is that computer science has grown out of logic. It is helping to suggest new ideas for logical analysis and these logical ideas are, in turn, allowing computer science to develop further. The two subjects have each contributed to the growth of the other and still are, and in combination they form an exciting and rapidly growing field of study. 1.2. Background history In the middle of the last century Boole laid down what we now see as the mathematical basis for computer hardware and propositional logic, but the logics that we are going to look at really started towards the end of the century with the work of Gottlob Frege, a German mathematician working in relative obscurity. Frege aimed to derive all of mathematics from logical principles, in other words pure reason, together with some self-evident truths about sets. (Such as 'sets are identical if they have the same members' or 'every property determines a set'). In doing this he introduced new notation and language which forms the basis of the work that we shall be covering. Until Boole and Frege, logic had not fundamentally changed since Aristotle! Frege's huge work was (terminally) criticized at its foundations by Bertrand Russell who found a basic flaw in it stemming from one of the 'self-evident' truths upon which the whole enterprise was based. However, Russell developed the work further by suggesting ways of repairing the damage. He also introduced Frege's work to the English-speaking mathematicians since not many of them, at that time, read German. Russell, who did read German, saw that the work was important and so publicized it. 1.3. Background terminology We are going to be doing what is usually known as 'mathematical Logic' or 'symbolic Logic' or 'formal Logic'. That is, we are going to use ordinary, but careful, mathematical methods to study a branch of mathematics called Logic. Before we start to look at what Logic actually is we shall try to make the context in which we are working a bit clearer. To make the discussion concrete we can think in terms of the typical introductory programming course that you may have followed. Such a programming course not only teaches you how to use the constructs of the language to produce the effects that you want when the program is executed, but it also teaches you the distinction between the language that you write programs in and the meaning of the statements of that language in terms of the effect that they have when executed by a computer. If the course was a good one, it will also have taught 3 you how to reason about programs - perhaps to show that two apparently different programs are equivalent. Logic is the study of formal (i.e. symbolic) systems of reasoning and of methods of attaching meaning to them. So there are strong parallels between formal computer science and logic. Both involve the study of formal systems and ways of giving them meaning (semantics). However in Logic you study a wider variety of formal systems than you do in Computer Science, so wide and so fundamental that Logic is used not only as one of the mathematical tools for studying programming, but also as a foundation for mathematics itself. This ought to set the alarm bells ringing, because we have already said that we were going to use mathematics to study Logic, so there is an apparent circularity here. It is certainly the case that circular or "self-referential" discussion like this is very easy to get wrong but the notion of self-reference is a central one in Computer Science and, in fact, is exploited rather than avoided. In Logic we deal with the issue by putting the logic we are going to study in one compartment and the logic we are going to do the studying with in another. These compartments are realized by using different languages. The logic that is the object of our study will be expressed in one particular language that we call the object language. Our study of this logic and language is carried out in another language which we call the observer's language. (You might also see the word metalanguage for this.) The idea should already be familiar to you from studying foreign or ancient languages. In this case Latin, for example, might be the object language and your native language, in which you might have discussed the details of Latin syntax or the meaning of particular Latin sentences, is the observer's language. In mathematics, the symbolism of calculus, set theory, graph theory and so on, provide the object language and again your native language, augmented perhaps with some specialised mathematical vocabulary, is used as the observer's language. In programming, the object language is a 'programming' language such as Pascal, Lisp or Miranda and the observer's language is again your native language augmented with the appropriate mathematical and operational notions. Example 1.1 Consider the statement times 0 do print* od = donothing 4 NTRODUCTION !! This, in fact, is a statement in the observer's language about the equivalence of two statements in one of our local programming languages. Although you may have guessed correctly, you have no means of saying with certainty which are the symbols of the object language and which are symbols of the observers language until the object language has been defined for you. In fact, the distinction is as shown in Figure 1. Exercise 1.1 Now you are invited to use your linguistic, mathematical and programming experience to do a similar analysis of the following statements into observer and object languages. (a) The sentence 'They feeds the cat' is ungrammatical in English. (b) The French translation of the English phrase 'Thank you very much' is 'Merci beaucoup' (c) The equation E=mc holds in Special Relativity. (d) There is no real value of x that satisfies x -2x + 2 = 0 (e) There is no real value of foo that satisfies x -2x + 2 = 0 (f) If x - 2x + 1 = 0 then x = 1 2 (g) If x - 2x + 1 = 0 then x must be 1 (h) If x - 2x + 1 = 0 then x must be unity (i) "E=mc holds in Special Relativity" cannot be proved. (j) The statements x:=x+1; x:=x+1; are equivalent to x:=x+2; in Pascal. (k) "if…then…else" is a statement form in Pascal You probably found that one or two of these exercises were borderline cases and caused you to point out, more or less forcibly, that it would be a lot easier if you 5 had an actual definition of the object language in front of you. This is the first thing we do when we embark on the development of propositional logic in Chapter 2. 1.4. Propositions, Beliefs and Declarative Sentences The basic items that logic deals with are propositions. Philosophers have given a variety of answers to the question "What is a proposition?" but since we are dealing with the mathematics rather than the philosophy of logic it doesn't really matter for our purposes. One answer, however, is that a proposition is what is common to a set of declarative sentences in your native language that all say the same thing. Philosophers then have to argue about what "all say the same thing" means, but fortunately we don't. Propositions communicate judgements or beliefs and since beliefs are themselves manifested as states of mind (it's hard to see what else they could be) the act of believing or the stating of propositions allows, with practice, the representation in your mind of complex objects both physical and abstract. We seem to be a long way from the limits of the human race, as a whole, in representing things mentally, and reasoning with them, and we are in the Stone Age when it comes to building ourselves tools for doing so. This is why the study of formal methods of manipulating propositions, Logic in other words, is so important. Since Computer Science is one discipline in which the objects that we want to reason about are extraordinarily complex, and often abstract and purely formal, the need for Logic here is especially clear. Of course, the fact that beliefs are states of mind means that we cannot directly manipulate them, neither can we manipulate propositions, since they are expressions of those states of mind. What we do is to manipulate sentences in some language which map on to propositions and beliefs. The language with which we, the authors, are most familiar for this task is the natural language called "English". We use it to express our beliefs as propositions, for the purpose of transferring them to each other, testing them and so on. When one of us says to the other "I believe that Moto Guzzi manufacture the best motorcycles in the world" he conveys part of his current state of mind, in particular a part that expresses a certain relation between himself and motorcycles. In general, then, we use English to express our beliefs. However, we need to refine this statement since English is rather complicated and not all of English is used for this purpose. There are only certain sentences in English that convey beliefs, i.e. express propositions, and these are the declarative sentences. 6 NTRODUCTION Definition 1.1 A declarative sentence is a grammatically correct English sentence that can be put in place of '…' in the sentence "Is it true that …?" with the effect that the resulting sentence is a grammatically correct English question. One might expect further restrictions here, though. The definition has a rather syntactic bias to it, and English is notoriously expressive. We cannot go into it fully here, but a good introductory discussion can be found in Hodges (1977). Exercise 1.2 Decide whether the following are declarative sentences or not: (a) What is your name? (b) Close the door! (c) Grass is green. (d) Grass is red. (e) It is wrong. (f) I am honest. (g) You must not cheat. (h) It is false that grass is red. 1.5. Contradictions By this stage you should have some feel for how beliefs are manipulated in natural language. But how are beliefs actually useful? What is their reason for existing? Basically beliefs give a description of the world as it is or might be. For example, if I have a system of beliefs about the laws of mechanics (a description of part of the world) I can generate beliefs about the Solar System without having to actually go out there and make measurements. If I have a system of beliefs about my friends, I can predict their behaviour in certain situations without the possible embarrassment of engineering and being in those situations. Again, I can have a set of beliefs about numbers and reason about the result of the sum 2+2, without actually creating two different sets of cardinality 2, amalgamating and counting them. So systems of belief allow decisions to be made, facts to be conjectured; it seems that they can do anything. However, there is one limitation. You cannot simultaneously hold two different beliefs which you know contradict one another. Since we have said that Logic is important because it allows us to manipulate beliefs, it follows that a fundamental task of Logic is to be able to decide whether or not a set of beliefs is contradictory. In simple cases, as we shall see, Logic can do this in a 7 mechanical way. But there are inherent limitations and it may be that, ultimately, even the most ingeniously programmed machine cannot do as well at manipulating propositions as the most careful person. This belief has not yet been contradicted! 1.6. Formalization Formalization is the process of constructing an object language together with rules for manipulating sentences in the language. One aim in doing this is to promote clarity of thought and eliminate mistakes. Another equally important issue, one that gives rise to the term "formalization" itself, is that we provide a means of manipulating objects of interest without having to understand what we are doing. This sounds at first like a retrograde step, but to give an example: arithmetic arose out of the formalization of counting. So we now have a set of rules which we can follow to add together numbers correctly without needing to understand what numbers are or what adding up is. Of course, we can always go back to the original physical act and see that adding up comes from the process of counting up to a particular number n with reference to one group of objects and then starting from n+1 in counting a second group. The answer in this case is what we would formally call the sum of the numbers concretely represented by each group. So the power of formalization is that, once formalized, an area of interest can be worked in without understanding. If the agent following the rules is a human being this might be a mixed blessing, since understanding at the intellectual level is a strong motivation for getting things done. But, if you want to write a computer program to reason, then formalization is essential. Equally essential, if the results are to be useful, is to be able to prove that, as long as the rules are correctly applied, the results will be correct. For instance, a programmer employed in the financial sector may have, in the form of a set of beliefs that are related in complicated ways, an idea of how the Stock Exchange works. It is the abstract structure of these relationships which models the concrete structure of the Stock Exchange and forms a model of how the Stock Exchange works. The programmer will then formalize this model when writing a computer system to automatically deal in the Stock Exchange, say. Now, if you look at the program, it is clear that the names of the objects in the program do not matter. Nor does the language in which they are written. What matters is that the relationships in the real thing are faithfully and fully represented in the program. This 8 NTRODUCTION is the sense of formalization that we are concerned with: the program should model the form of the real thing in interaction between its parts. In the next chapter we make a start by looking at a simple form of declarative sentence and we show how it can be used to formalize some basic instances of reasoning. Summary • Mathematical logic began towards the end of the last century when Frege developed what is now the predicate calculus. • Mathematical logic involves applying standard mathematical methods to the study of systems that themselves can be used to formalize mathematics. The apparent circularity is overcome by distinguishing between the object language, in which the formal system is expressed, and the observer's language in which properties of the formal system are expressed and reasoned about. • The basic items that logic deals with are propositions. Propositions are used to express beliefs. In natural language they are represented by declarative sentences. • The notion of belief is a very general one; nevertheless there are some restrictions on the way beliefs can be manipulated in mental reasoning. For example you cannot simultaneously hold contradictory beliefs (at least without being aware that something is wrong). • The importance of formalization is that once a particular area of mathematics or computer science has been formalized, reasoning in it can be carried out purely by symbol manipulation, without reference to meaning or understanding, and mathematical properties of the reasoning process can be clearly stated and proved. CHAPTER TWO Formalizing the Language 2.1 Informal Propositional Calculus 2.1.1 The language We will use Æ, Ÿ, ⁄, ! and ´ as our standard symbols for the connectives. These symbols form part of the alphabet of the language of propositional logic. Other elements of the alphabet are the parentheses, ) and (, and a set of propositional variables, for instance {p, q, r, s}. We can now give a proper definition of the conditions that a sequence (string) of symbols must satisfy to be a sentence of propositional logic. Definition 2.1 If P is a set of propositional variables then: 1) a propositional variable from the set P is a sentence, 2) if S and T are sentences then so are (¬S), (S Ÿ T), (S ⁄ T), (S Æ T) and (S ´ T), 3) no other sequences are sentences. We can, for example, use the definition to show that p, (p Æ q), (p Ÿ (¬q)) and ((p Ÿ q) Æ r) are sentences, because p is a sentence by clause 1, since p is a propositional variable, (p Æ q) is a sentence because p and q are sentences by clause 1 and hence, by the fourth condition in clause 2, the whole string of symbols is a sentence. The other cases follow similarly. 9 10 FORMALIZING THE LANGUAGE In practice, to keep the number of brackets to a minimum, there is a convention that ¬ takes precedence over or, as it is sometimes put, "binds more tightly" than Ÿ and ⁄ , which in turn bind more tightly than Æ and ´. Also, outside parentheses can often be omitted without ambiguity. So (p Ÿ (¬q)) would usually be written as p Ÿ ¬q and ((p Ÿ q) Æ r) as p Ÿ q Æ r. Furthermore, we can see that ¬p), for instance, is not a sentence since, although we have that p is a sentence (clause 1), none of the other clauses makes ¬p) a sentence so by clause 3 it is not a sentence. The set of symbol sequences (strings) defined in this way is called the set of (well-formed) sentences or language of propositional logic. The form of the definition is important not only because it is the first of many that we shall be seeing, but also because it determines the property of "being a sentence of propositional logic" as being decidable. That is, the question "is this sequence of symbols, formed from the alphabet of propositional logic, a sentence of propositional logic?" can always be answered correctly either "yes" or "no". Later on we shall see some similarly structured questions which cannot be answered in all cases. These will be called undecidable questions. There are two ways to be sure that this (or any) definition gives rise to a decidable property; you can either construct a proof that it is so or you can construct a program which always gives the correct answer to the question "is this string a sentence?". By "always gives the correct answer" here we mean that, whenever the question is asked, the program answers it correctly before it terminates - and it always terminates. Clearly, to implement the definition as a program involves much more work than only proving that the definition gives a decidable property, but for the extra work we gain a program that can always answer the question correctly without further work on our part. With a suitably expressive programming language we can use the above definition, of sentences based on the set P of propositional variables, to give us almost directly a programmed decision procedure. First, though, we have to represent the forms of sentence defined by the grammar in the language that we will use. In this book we use two programming languages, SML and Prolog, that are becoming widely used in computer science for implementing algebraic and logically based calculations. These languages are also theoretically interesting in their own right. SML is based on the l-calculus and type inference, while Prolog is abed on the notion of logic programming (see Chapter 7). An introduction to each of the languages is given in Appendix A. Using the datatype feature of SML makes it easy 11 to define all the possible forms of sentence. For instance, just as the definition above uses the phrase ‘…if S is a sentence then so are (¬S) and …’ then we can use the phrase ‘…S = Not of S |…’ in SML to represent the same idea. Notice that instead of using the symbol ‘¬’ we have used the symbol ‘Not’; this is done so that later on when we write programs to manipulate these sentences we do not get too many, possibly confusing, sequences of symbols, that is we prefer the words. So using datatypes the type SENT, which represents sentences of the language, can be defined in SML as: Datatype SENT = Prop of string | Not of SENT | And of (SENT * SENT) | Or of (SENT * SENT) | Imp of (SENT * SENT) | Eq of (SENT * SENT); This means that a sentence, that is a value of type SENT, is either of the form Prop (“p”) or Not (S) where S is a value of type SENT, or And (S,T) where S and T are both values of type SENT, and so on. The way in which this declaration represents sentences as defined above should now be clear. Of course, writing down sentences using the form described in this declaration is not as convenient fro us as the from in the original definition since there is more to write. But we must remember that the language SML is fixed (and completely formal, of course) whereas we, as humans, have a certain amount of flexibility when it comes to adapting ourselves to other notations. So, since the programming language will not adapt, we have to. However, it is usual to mitigate the somewhat verbose programming representation of the components of a language when, say, non-specialists have to use it by putting a piece of software called a parser between the user and the program being used. The task of the parser is to take a string of symbols from the user and, for those that are suitable, to transform them into the required form from the programmer’s point of view. Thus, we would, in any suite of programs to do things as yet unspecified with logical statement, expect to have to write a program which carried out this task. It turns out that to do this task properly is not a trivial thing. However, parsers are such important and ubiquitous pieces of software that a lot of effort as gone into making their design fairly routine. In the SML programs that we 12 FORMALIZING THLANGUAGE write in the rest of the text we will be using just the internal from of the language, but in Appendix B we have given the text of a parser so that the interested reader may see what is required to implement such a program. It is not, however, necessary to understand how the parser works, or even to acknowledge its existence, in order to understand what follows, so the uninterested reader need not worry. (In fact, by defining the constructor symbols to be infixed, we can circumvent the need for a parser somewhat, which is just what we do below in Prolog, but since this was a good please to bring to the reader’s notice the idea of parsing we decided on the current presentation.) Having represented the sentences we can now go on to describe how to do computations with them. First, consider the problem of deciding whether a string is a sentence based on a set of the definition above but given in SML: fun decide P (Prop v) = v memberof P | decide P (Not(l)) = decide P l | decide P (And(l,r)) = (decide P l) andalso (decide P r) | decide P (Or(l,r,)) = (decide P l) andalso Pr) | decide P (Imp(l,r)) = (decide P l) andalso (decide P r) | decide P (Eq(l,r)) = (decide P l) andalso (decide P r); We can see that the program always terminates since it either returns a value (true or false) immediately or, if a recursive call is made, the arguments of the recursive call are strictly smaller, as pieces of text, than the preceding number of recursions, so the program will always terminate. The correctness of its answer follows from the closeness of the program to the original definition. We conclude, therefore, that the property of being a sentence of propositional logic is decidable. 2.1.2 The Prolog version of ‘decide’ and the enumeration of sentences In Prolog (and again see Appendix A for details of the language) the decision procedure can be expressed as :-op(510, fx, [ ~ ]). :-op(520,xfy, [/ \ ]). :-op(530,xfy, [\ / ]). 13 :-op(540,xfx, [’ ]). :-op(550,xfx, [÷]). member(X,[Y|Z]):-X = Y;member(X,Z). decide(S):-member(S,[p,q,r,s]). decide(~S):-decide(S). decide(S):-(S=Q)/ \ R;S = Q \ / R;S=Q’R;S=Q÷R), decide(Q),decide(R). The major difference between the SML and Prolog versions is that with Prolog we define a relation rather than a function, but it should nevertheless be apparent that the programs are essentially the same operationally and what was said above about the recursive calls, termination and decidability applies equally here. Prolog allows you to define your own infixed operators and this program is complete and can be used as it stands, without the need for an additional parser. We have taken the opportunity to invent some symbols for the logical connectives that we use in this book. The first five lines of the program are system-defined predicates fro specifying the precedence and associativity of the operators and you will find an explanation of this in Appendix A or any good book on Prolog. Prolog programs are used by expressing a request for a computation as a goal (again, see Appendix A for more practical, and Chapter 7 for more theoretical, detail). For example to use the program above to check whether or not the string of symbols p/\q -> r is a sentence of the language, you type ?-decide(p/\q -> r). to which the prolog interpreter would out put ‘yes’, whereas for ?-decide(p+q). you would get the output ‘no’, and for ?-decide(->p). you would be told that there is a syntax error because the connective -> is defined to take two arguments. 14 F ORMALIZING THLANGUAGE As well as the question of decidability another important property is that the sentences of prepositional logic are enumerable, that is all the sentences that get the answer ‘yes’ can be arranged in a list with a first member, a second member, and so on. With a little experience of Prolog one might think that the backtracking mechanism could be used to generate this list by repeatedly satisfying the goal ?-decide(S). However, this does not work because of the fixed-order, depth-first nature of Prolog’s execution model. With two prepositional variables p and q you would, in fact, get the output p; q; ~p; ~q; ~~p; ~~q; ~~~p; and so on ad infinitum. Because the program clauses dealing with ~ come before those dealing with the other connectives, a formula such as p/\q can never be generated. It is clear that simply reordering the clauses will not help either. One way to get round this is to use an idea invented around 1880 by Georg Cantor. Cantor wanted to find out if all infinite sets are the same size (they are not in fact), and he defined a set as enumerably infinite if it could be put into one-to- one correspondence with the positive integers. He noticed a similar problem to the one we have encountered here arises with the rationals, that is numbers of the form i/j where i and j are positive integers. If you start listing them in the order 1/1, 2/1, 3/1,… you will never, for example, get to 1/2. Cantor’s way around this was to imagine the rationals arranged in a two-dimensional array in which i/j is in the ith column and the jth row (the diagram following shows the idea.) 1 2 1 1/1 2/1 3/1 2 1/2 2/2 3/2 3 1/3 2/3 3/3 4 1/4 2/4 3/4 5 1/5 2/5 3/5 … … … The idea is to enumerate the elements of the array by starting at the top left-hand corner with 1/1 and following the path shown to give the list 1/1, 2/1, 1/2, 3/1, 2/2, 1/3, 4/1, 3/2,… . It is intuitively clear that by doing this you eventually get to any point i/j. If intuition does not satisfy you, as indeed it should not if you are going to study logic, then it is straightforward by elementary algebra to show that i/j is in position (i + j – 2)(i + j –1)/2 + j in the list. Conversely, we can invert the mapping to show that the nth rational in the list is i/j where j = n – (k – 2)(k – 1)/2, i = k – j and k = Î(3 + 8n – 7 ) /2 ˚ . We can use the same idea to enumerate logical formulas. To keep things simple for the moment suppose we have only one connective, f say. Then, following the recursive scheme given above, we know that any formula is either a sentence letter or of the form (S fT) where S and T are both formulas. Now we do exactly the same as for the rationals. (S fT) is in the column corresponding to S and the row corresponding to T. The propositional variables count as formulas, of course. If they are finite in number then they can be listed before all the compound formulas. If we have an infinite supply of propositional variables then there is a slight complication because we must ensure that any given one is eventually brought into use. One way round this is to place the propositional variables at odd numbers in the list, with compound formulas at the even-numbered positions. The top left-hand corner of the array of 16 ORMALIZING LANGUAGE compound formulas would then, for propositional variables p, q, r,… be as in the following diagram (we have as usual omitted the outermost pair of parentheses). p p f p p p f p (p f p) f p p f p p f (p f p) (p f p) f (p f p) q f (p f p) q p f q (p f p) f q (p f p) f p p f ((p f p) f p) … We can now use exactly the same scheme of enumeration as we did for the rationals to generate the list of formulas p f p, (p f p) f p, p f (p f p),.. which, when merged with the sentence letters, will be in positions 2, 4, 6,…. We can imagine this mapping to be a code, a function c say, that takes integers to formulas. As above it is straightforward to show that c(S f T) = (c(S) + c(T) – 2)(c(S) + c(T) –1) +2c(T) and, for n even, d(n) is d(i) f d(j) where j = (n – (k – 2)(k – 1))/2, i = k – j and k = Î3 + 4n – 7 ) ˚2 . We can then write these functions as Prolog predicates and, by enumerating the integers in increasing order and decoding them into formulas, we can realize our original goal of demonstrating an effective rpocedure for enumerating all the sentences of the language—or in practical terms, as many as we want. :-op(540,xfx,[->]). int(1). int(K) :- int(J), K is J+1. split(N,I,J) :- int(K), L is K * (K-1), L>=N,!, J is (N-(K-2) * (K-1))//2, I is K-J. code(S,N) :- atom(S), name(S,[I]),N is 2 * I – 193. code(S->T,N) :- code(S,I),code(T,J), N is (I+J-2)*(I+J-1)+2*J. 17 decode(N,S) :- 1 is N mod2,!, I is (N+193)//2,name(S,[I]). decode(N,S->T) :- split(N,I,J), decode(I,S),decode(J,T). enumerate(N) :- int(K),L is 2*K, decode(L,X),write(X),nl,K>=N. This is a complete program for coding, decoding and enumerating sentences that will work as it stands. It will be seen that it includes some features of Prolog that are of no logical interest, but are necessary to manipulate numbers and symbols at a basic level. The name predicate for example is a system utility for splitting an atom into a list of characters. It is used here to generate propositional variables starting at the letter ‘a’ (193 being twice the internal numerical code for ‘a’ minus one). The split predicate does the square root computation by a method of testing that uses only interger arithmetic. It could be replaced in most Prolog systems by the system’s square root operator. Of course, enumerating all possible sentences is not much practical use but, in the theoretical study of what the limits of computation are, it is important to show that you can in principle carry out such an enumeration . Furthermore, the idea that you can code formulas using arithmetic is an important one in its own right, quite apart from its use here for enumeration. In one of the most significant results in the history of mathematics Gödel used the idea to show, in 1931, that any logical basis for arithmetic is bound to be inadequate in a certain technical sense. We shall say a little more about this later. Exercise 2.1 (a) Work out how you might modify the Prolog program for enumerating sentences with -> so that it could handle the complete set of connectives ~, /\, \/, ->, <->. th (b) Calculate by hand what the 1000 compound sentence is, that is what d(2000) is. (c) Write a similar program for enumerating sentences in SML. 18 FORMALIZING THE LANGUAGE 2.1.3. Giving meaning to the language So far we have defined the form of the language that we are studying. We can now decide whether or not a string of symbols from the alphabet is a well-formed sentence of this language. However, we do not yet have a way of giving any meaning or semantics to these sentences. It is as if you had been given a manual for Pascal with the part that gives the meaning, usually a set of rules that tell you how a given statement is executed (known as operational semantics), omitted from the manual. You would be in a position to write programs that were correctly formed, as far as the Pascal syntax is concerned, but you would not know what the program denotes or what its effect would be. You would not know its meaning. At this point we are in a similar position with propositional logic; we can write well-formed sentences but we cannot say what they mean or relate them to any other language. To give a meaning to a language we first have to associate the sentences of the language with some class of objects. For instance, in English, we begin our acquisition of language with simple utterances that consist of single words: "Dog!", "Cat!", "Car!" etc. Our understanding of the meaning of these words is judged by our use of them. That is, we say that someone understands the word "cat" if they point to a cat as they say it. If someone points to a cat and says "Dog!" then we conclude that they do not understand the meaning of the word. At this simple level, at least, we can imagine that there is a mapping between the words and the objects that they denote. Then, as our natural language develops, we understand words for verbs, adjectives, relations and so on. Again, our understanding is demonstrated by our use of the words in certain situations. Of course, a natural language like English is far more complicated than any artificial language (such as a programming language or a logical language) and, although our methods will allow us to give a semantics to the languages that we shall study in this book, it is not yet, and may never be, possible to give a semantics to English in the same manner (if only because the language is not static). So we have first to decide what objects, perhaps in an abstract sense, we are to have our sentences denoting. For the moment we are going to make an assumption that will mean our semantics is classical. The assumption is that any sentence is - has for its meaning something that is - either true or false. To make the meaning of 'true' and 'false' absolutely clear we can do what we do when telling someone the meaning of any other word - we can point to an instance. In this case, to explain our usage of 'true' and 'false', we refer you to statements that we can confidently assume you will 19 recognise as true and false. Every reader can be assumed to know that the numbers one and zero are not equal.So we can say that what a sentence refers to will either be the same thing that the arithmetic statement "0=0" refers to or it will be the same thing that the arithmetic statement "0=1" refers to. Here we are taking a view of semantics that is called denotational - we say what each sentence in the language denotes. Contrast this with what was said earlier about Pascal, where we spoke of the semantics of the language being specified by the actions that can be attributed to a particular sentence of the language, known as operational semantics. As it happens, Pascal is a simple enough language for it to be given a denotational semantics too, although quite a lot of work had to be done before the underlying mathematics was properly worked out. We could contemplate giving an operational semantics to our propositional logic in which, perhaps, one action was performed and called 'true' and another was performed and called 'false' depending on whether the result of testing a value in a computer register is what we conventionally call true or false. It turns out, however, that such an operational approach is too cumbersome when all we really want to work with are abstract notions such as truth and falsity. The idea of letting truth reside in a particular action involves all the detail of how the action is carried out, how long it takes and what happens if it goes wrong. For other purposes, particular those involving getting an effect when you execute a program, like an invoice being printed or a line drawn on a screen, the operational detail is vital; but here it just complicates matters, so we take the denotational approach. Every sentence of the language is either true or false, so we need rules for calculating which of these two values a given sentence has. The situation here is similar to the usual algebra of arithmetic where we have operations like multiplication and addition, symbolized by * and +, and letters such as x and y which are understood to stand in place of numbers. In propositional logic we have five operation symbols and a quantity of sentence variables that can stand in place of sentences. Just as we can give a meaning to an algebraic statement in terms of the meanings, or denotations, of the operation symbols, which operate on numbers, so we can give a meaning to the logical operators, which here we call connectives, by saying how they act on the denotations of sentences, i.e. on truth and falsity. 20 FORMALIZING THE LANGUAGE 2.2 Arguments 2.2.1 Informal arguments A notion that is central to our work is that of argument. The language that we introduced above will allow us to express, and show valid, arguments such as If Socrates is a man then Socrates is mortal. Socrates is a man. Therefore, Socrates is mortal. It should not allow us to show valid the argument Socrates is a man. Therefore, Socrates is mortal. even though, by knowing the meaning of the words, we would say that the conclusion holds. If the textual form of the argument is changed to If Ssss is an xxxx then Ssss is a yyyy. Ssss is an xxxx. Therefore Ssss is a yyyy. we can guarantee that you cannot make an assessment of the argument from its meaning, yet we anticipate that you will accept it as valid by virtue of its structure. So we are going to judge the validity of arguments by their form, not their meaning. This means that even the following argument is valid: Paris is in Australia and Australia is below the equator Therefore, Paris is in Australia because its form is that of a valid argument, even though your geographical knowledge tells you the conclusion is false. Also, the following argument is not valid despite all the statements, including the conclusion, being true: The Eiffel Tower is in Paris or Paris is in France Therefore, the Eiffel Tower is in Paris 21 So, the correctness of an argument is not governed by its content, or its meaning, but by its logical form. We are going to make this idea much more precise and at the same time abstract away from the particular statements involved in the arguments, which makes the form much clearer. Exercise 2.2 1) Say whether each of the following arguments is valid or not. a) The Eiffel Tower is in Australia and Australia is below the equator Therefore, The Eiffel Tower is in Australia b) The Eiffel Tower is in Paris or Paris is in France Therefore, the Eiffel Tower is in Paris c) The Eiffel Tower is in Australia or Australia is below the equator Therefore, the Eiffel Tower is in Australia d) The Eiffel Tower is in Paris and Paris is


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.


You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

Why people love StudySoup

Steve Martinelli UC Los Angeles

"There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

Janice Dongeun University of Washington

"I used the money I made selling my notes & study guides to pay for spring break in Olympia, Washington...which was Sweet!"

Jim McGreen Ohio University

"Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

Parker Thompson 500 Startups

"It's a great way for students to improve their educational experience and it seemed like a product that everybody wants, so all the people participating are winning."

Become an Elite Notetaker and start selling your notes online!

Refund Policy


All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email


StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here:

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.