Phew. Last week was not an easy week. Especially for those of you seeing formal proofs for the first time. The good news is that, once you get the hang of it, doing proofs becomes a lot easier. Moreover, you can take comfort in knowing that our proof methods are sound and complete. If you manage to find a formal proof of a conclusion, the conclusion *must* be logically entailed; there can be no mistake. Also, if a set of premises logically entails a conclusion, it is always possible to find a formal proof of that conclusion.
A word about the Fitch system used in the course. The rules in this system are easy to use (though it is not always easy to know which ones to use to get a particular result). This contrasts with other systems where just figuring what the rules do is difficult. We chose this version because we thought it would help you learn about the methods, the difficulties, and the joys of doing proofs (when you finally succeed). The system can easily be elaborated with lots of additional rules of inference, making it a lot easier to use on practical problems. There is even a version that supports user-generated rules and meta-theorems, which make it possible to re-use earlier proofs when trying to prove more complicated results. But, before giving you these power tools, we want you to understand the basics.
If you want more practice with proofs, you might show the following results. Those in the first group are trivial. Those in the second group are not trivial but still relatively easy; just be sure you are comfortable with them. Those in the last group are difficult.
This week, we look at another proof system - Propositional Resolution. Like Fitch, Propositional Resolution is sound and complete for Propositional Logic, i.e. everything that is provable is logically entailed and everything that is logically entailed is provable. However, Propositional Resolution is much simpler to use than these other proof systems, and proofs are frequently shorter than proofs in Fitch. For example, given p|q and ~p, it takes multiple steps or so to prove q in Fitch, whereas this can be done in 1 step in Propositional Resolution. That said, some people criticize Propositional Resolution because the proofs are sometimes less intuitive than Fitch proofs. Chacun a son gout. You will either love it or hate it. In any case, it is particularly useful for automating theorem proving - computers love it! And, by the way, it is equivalent to the simple rule of inference we looked at in the Introduction.
Don't forget that the midterm examination will be take place this week. To be clear, it will cover material on chapters 1-5 (inclusive) of the notes. Closed book. No computers. Brains and pens or pencils only. 12:00 to 1:20 this Thursday in Gates B01. Be there or be square.
No puzzle this week. Spend your time preparing for the midterm. After the quiz, we will have some weekly puzzles that are significantly more difficult than any of those you have seen thus far.
By this point, you should have mastered the material in Lessons 1 through 3. From the Introduction, you should be familiar with the main topics of the course - logical languages, logical entailment and logical reasoning, formalization, and automation. From Lesson 2, you should understand the syntax and semantics of Propositional Logic and the notions of evaluation and satisfaction. From Lesson 3, you should understand the concepts of validity, contingency, and unsatisfiability as well as logical equivalence and entailment and consistency.
In fact, you should be more than familiar with this material - ideally, you should be saying to yourself (and others) that, when all is said and done, this stuff is pretty easy. In fact, it *is* easy. There is more difficult material to come; but hopefully, after we have gone through it all, you will think that that is easy too!
This week, we finally get to logical reasoning - rules of inference, linear proofs, hypothetical proofs, and the Fitch system. By the time you are done this week, you should be comfortable doing Fitch proofs; and you should be ready to opine about its strengths and weaknesses.
All of the exercises this week require that you do formal proofs, and many of you will find these exercises to be more challenging that the exercises in preceding weeks. Just remember, when you are doing a proof, first formulate a plan for the proof. Often, this means starting at the end and thinking about how to derive the desired conclusion and then figuring out how to prove the intermediate results you need to prove the final result. If you are having trouble, don't forget to stop by the discussion sessions on Tuesday and/or Thursday.
In case you need a break from proofs, there is a new puzzle for you to work on this week - Nations. This one is relatively easy like the last few puzzles, but there are some more challenging ones coming.
Sharpen your pencils and get out your copybooks; the course begins in earnest now. This week, your goal is to master the material in lessons 2 and 3.
Lesson 2 introduces the syntax and semantics of Propositional Logic as well as the essentials concepts of evaluation and satisfaction. You should get comfortable with the language and you should get comfortable evaluating sentences and finding truth assignments that satisfy those sentences.
Lesson 3 deals with the logical properties of sentences, e.g. validity and satisfiability. And it introduces and distinguishes the central notions of logical equivalence and logical entailment and logical consistency. These ideas are all fairly simple in the context of Propositional Logic; they are more subtle in the context Relational Logic and Herbrand Logic. It is a good idea to ensure you understand them thoroughly before we get to those more complicated logics later in the course.
Note that there are some useful tools available under the Tools tab, notably Babbage (for generating simple truth tables) and Boole (for generating multicolumn truth tables).
Puzzle of the week - Logicians. This one is probably the easiest of the course. Red hats and black hats. Who is wearing which?
Okay. We are on our way! The course begins now. On Tuesday, we will have an introductory lecture on the subject matter of the course and course logistics. On Thursday, we will have our first in-class discussion session.
Your goal this week is to read through the first lesson. This is just an overview, and it is a very easy read. That said, you should not shortchange the material. The lesson talks about the main ideas of Logic and how they relate to each other, and it provides a framework for organizing the rest of the material in the course. After this week, things get more challenging and increase in difficulty as the course goes on, so do not fall behind.
Be sure to do the exercises. This week's exercises are extremely easy. They are there mostly for you to get experience with the technology so that you will be ready to deal with the increasingly substantive exercises to come.
You should also drop by Piazza to check out what others in the class are saying. There are some subtleties in Logic that you can miss and that can lead to confusion. Engaging in discussion on the Piazza forum is a good way to deal with thee subtleties. And, even if you think you understand you, you might consider using Piazza to help others and thus consolidate your understanding of the issues.
Finally, you might want to check out the puzzles. There are eight of these in all, and we will release then one per week. This week's puzzle is Coins. Some of the puzzles are easy; others are more difficult. They are not directly tied to the course material, but there is a strong relationship and solving them does require the techniques discussed in the course. The puzzles are not a required part of the course, but in the past students have found them worthwhile and enjoyable.
CS 157 is a rigorous introduction to Logic from a computational perspective. It shows how to encode information in the form of logical sentences; it shows how to reason with information in this form; and it provides an overview of logic technology and its applications - in mathematics, science, engineering, business, law, and so forth. Topics include the syntax and semantics of Propositional Logic, Relational Logic, and Herbrand Logic, validity, contingency, unsatisfiability, logical equivalence, entailment, consistency, natural deduction (Fitch), mathematical induction, resolution, compactness, soundness, completeness.
This year, we are continuing our experiment with a "flipped classroom" approach to teaching the course. You are expected to go through the online course materials on your own time. There will be no traditional lectures during class time. Instead, we will use that time for review, problem solving, and general discussion.
All of the materials for the course are accessible via "Intrologic" tab at the top of this page. There are links to lessons, interactive exercises, a glossary, logic puzzles, and some logic tools. In order to access this material, you will need to sign up on the site. Please use your Stanford email address, as we will use this correlate your work there with our class lists.
Note that, as you proceed through the online materials, you may occasionally encounter technical problems. Apologies in advance if this happens to you. We are still working on the course. You may get extra credit for reporting such problems (especially if your reports are more constructive than irate).
Collaboration with your fellow students is encouraged. Feel free to discuss the subject matter and the problems either in person or using Piazza. Our experience has shown that it is useful for students to work together to understand the material of the course and to do exercises. Such activity is both acceptable and encouraged. That said, you are expected to submit your own work in this course; and you are responsible for understanding and being able to explain any solutions you submit.
Your grade for the course will be based on your online results, an in-class midterm (during class on October 19 in Gates B01), and an in-class final exam (12:15 - 3:15 on Thursday December 14). The online results will count for 25% of your grade; the midterm, 25%; and the final, 50%. As preparation for the in-class exams, we highly recommend that you review the online exercises, as the problems on the in-class exams closely resemble these exercises.
© Copyright 2017 by Michael Genesereth. All rights reserved.