Propositional Logic ------------------- Recall that a logic is given by two components: 1) A notation to express propositions (or formulae, or "predictions") about artifacts of interest. 2) A means of verifying the truth of such predictions. Propositional Logic refers to systems of logic that include several standard constructs for combining formulae. Here is a data definition for the propositions of the logic that we'll study: P ::= P -> P ;; implication | P /\ P ;; conjunction ("And") | P \/ P ;; disjunction ("Or") | ~P ;; negation ("Not") | true | false | A ;; atomic formulae The atomic formulae A will vary depending on what we want to talk about with the logic. Maybe we'd like to discuss the weather: A ::= raining | snowing | sleeting | ground-wet Now we can express statements like: raining -> ground-wet raining -> snowing ;; probably not true, but expressible nonetheless ~(ground-wet -> raining). ~ground-wet -> ~raining ground-wet \/ ~ground-wet raining /\ snowing -> sleeting /\ ground-wet For us, we're interested in talking about equivalence of ACL2 programs, and so A will involve those: A ::= E = E ;; "atomic formulae" E ::= variable | 'C | (variable E ...) ;; <-- Expressions C ::= Number | String | Char | SymbolName ;; <-- Constants Example Propositions: '3 = '3 '1 = '2 -> '2 = '1 x = y -> y = x '3 = '1 -> (cons x y) = '42 (*) Side Note 1: Notation for numbers is a little strange - we are distinguishing numbers from numerals. Consider: III, three, tre, tres, drei, thrice one, |{a,b,c}|, '3, 11 binary. They are all just notations or _numerals_ that denote the _number_ 3. Sometimes we'll write 3 when we mean '3 (but never vice-versa!). So long as we're aware of the schizophrenia, no big deal. Side Note 2: Puzzle: given (implies (equal '3 '1) (equal (f x) '42)) Is this a proposition or an expression? It's an expression that reads much like a proposition. How is it related to the formula marked (*) above? They appear to be two ways of saying the same thing, and there is a close relationship. We will discuss the relationship later, but for now just be aware of the distinction betweeen propositions and expressions. Determining Truth ----------------- Now that we can express logical propositions that talk about interesting things, we need a way to determine truth. Let's just write a "program" called M that does the job! (We will write an informal mathematical function; the real program is your homework!) Note: I'll use both P and Q to stand for formulae. We'll use top and bot to represent truth values. To define M, we just follow the template for P just as we would if we were designing a program. (We did that in class, I'll just write the code.) ;; M : Proposition -> {top, bot} ;; determine truth of a formula (P) M[P -> Q] = if M[P] then M[Q] else top M[P /\ Q] = min( M[P] , M[Q] ) M[P \/ Q] = max( M[P] , M[Q] ) M[~P] = flip( M[P] ) M[true] = top M[false] = bot M[A] = alpha[A] where flip : {top, bot} -> {top, bot} flip(top) = bot flip(bot) = top min : {top, bot} {top, bot} -> {top, bot} min(top, top) = top min( X, Y) = bot, when X and Y are not both top. max is defined analogously; do it yourself! We know the contract & purpose of alpha, but we will ignore the examples, template, and code for now. ;; alpha : Atomic -> {top, bot} ;; determine truth of an atomic prop (A) alpha[A] = IGNORE FOR NOW Remember that the definition of alpha depends on what we want to talk about with our logic. For example, if we were talking about weather, then to evaluate alpha(raining), alpha must do the following: 1) Jump off of the page and walk over to a window. 2) Look out the window to see if it's raining. 3) Report back. If our atomic formulae deal with ACL2 programs, then alpha has to somehow determine when ACL2 programs are the same. We will ignore this complication for now. It turns out that we can get quite far in our study of propositional logic without nailing down such details! Note (INTERPRETATIONS): Logicians would call alpha an _interpretation_ for the atomic formulae. Important fact: propositions are only finitely big. That means that there are finitely many atomic propositions contained inside any given proposition. So in the case where we're dealing with a single proposition, we could represent an interpretation as simple data rather than as a function. For example, here is one possible interpretation for the atomic propositions defined as a function: alpha0['3 = '1] = top alpha0['1 = '3] = bot and here is the same interpretation represented as a list in ACL2: (list (cons <<'3 = '1>> <>) (cons <<'1 = '3>> <>)) I use <> to mean "some ACL2 representation of X". You'll have to come up with such representations for this week's homework, and you'll find the latter representation of interpretations useful. Look up the function _assoc_ in Help Desk to ease working with the list representation of interpretations. TRUTH TABLES ------------ Let's see how we can use our M from above to determine truth of propositions. For example, let's consider the truth of: '3 = '1 -> '1 = '3 /\ '1 = '3 -> '3 = '1 Abbreviate this proposition as P. We're interested in M[P], but how can we determine that without knowing an interpretation alpha? We will build a _truth table_. Truth tables enumerate the value of M[P] *for each possible interpretation (alpha)*. * How many atomic formulae in P? There are two: '3 = '1 and '1 = '3. * Alpha could produce top or bot for each one, so how many possible interpretations do we have? (Four.) We'll make one column for the interpretation of each atomic proposition and then one more for M[P]. Because there are four possible interpretations, we leave make four rows: alpha['3 = '1] alpha['1 = '3] M[P] -------------------------------------- ??? ??? ??? ??? ??? ??? ??? ??? ??? ??? ??? ??? Then we fill in all the possible interpretations. Each atomic formula could be assigned either top or bot: alpha['3 = '1] alpha['1 = '3] M[P] -------------------------------------- top top ??? top bot ??? bot top ??? bot bot ??? To fill in the M[P] column, we read across each row and compute using the definition of M. For example, in the first row, we assume alpha['3 = '1] = top and alpha['1 = '3] = top. Using that, the definition of M tells us that M[P] = top also. Here is the complete table: alpha['3 = '1] alpha['1 = '3] M[P] -------------------------------------- top top top top bot bot bot top bot bot bot top Let's try another example: (f x) = (g y) -> (f x) = (g y) Call that proposition Q. There is only one atomic proposition, and so there are only two possible interpretations: either it's top or it's bot. Thus we have two rows in the truth table. Here is the whole thing: alpha[(f x) = (g y)] M[Q] --------------------------- top top \_ note: doesn't matter what alpha is! bot top / Another example: Let A0 stand for (f x) = 'moo. A1 stand for (g y) = 'foo. Let P stand for A0 -> [A1 -> [A0 /\ A1]] Note: The brackets in P are just to show grouping explicitly. The truth table is: alpha[A0] alpha[A1] M[P] -------------------------- top top top \ top bot top |__ alpha didn't matter again! bot top top | bot bot top / Just one more example: Let A be (f x) = '2 Let P be A /\ ~A alpha[A] M[P] -------------- top bot \__ alpha doesn't matter yet again! bot bot / VALIDITY & SATISFIABILITY ------------------------- Formulae P for which M[P] = top on all the lines of its truth table are called _valid_. We abbreviate the phrase "P is valid" by writing |= P. Note: "P is a tautology" is synonymous with |= P. Formulae P for which M[P] is sometimes top are called _satisfiable_. No special symbol. Note that if |= P, then P is satisfiable. Formulae P for which M[P] = bot on every line in the table are called _unsatisfiable_. Formulae P for which M[P] = bot sometimes are _invalid_. We write a slash through the |= to indicate invalidity: |/= P. We've gotten pretty far without pinning down any particular interpretation (alpha). In fact, from here on out, we will simply use A, B, A0, A1, B0, B1, etc. to stand in for atomic formulae without choosing one particular formula. Using truth tables, we can say plenty of interesting things knowing neither the atomic propositions nor a particular interpretation!