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! INTERPRETATIONS AND MODELS -------------------------- Recall that an interpretation is a mapping from a set of atomic formulae to {bot, top}. When we wrote our function M, we just assumed there was a particular interpretation named alpha that "just worked". It's useful to abstract M over the interpretation. So from now on think of M like this: M : Proposition Interpretation -> {top, bot} where Interpretation = (A -> {top, bot}). We'll write application of M as M[P]_a (the _ is a convention that means "subscript"). A _model_ for a formula P is just an interpretation a such that M[P]_a = top. There is notation for "a is a model for P": |=_a P. This notation gives us another way to express validity: |= P if and only if |=_a P for all possible interpretations a. In other words, P is valid if and only if every interpretation models P. *Programming Note: Remember that in ACL2 you cannot pass functions around as values. So when you write programs that manipulate (finite) interpretations you'll just have to represent them differently -- for example, ;; Interpretation = List[(cons Atomic Truth)] (defconst *my-example-interp* '((A . t) (B . nil) (C . t)) ) You can "apply" such an interpretation to an atomic formula using the built-in function _assoc_. (equal (assoc 'A *my-example-interp*) '(A . t)) (equal (cdr (assoc 'A *my-example-interp*)) t) Look assoc up in Help Desk if you haven't already. Also, note that '(B . nil) prints out as (B) because nil is the empty list -- don't let that throw you off. COMBINED TRUTH TABLES --------------------- We can build a truth table for several formulae at once. Suppose A and B are two atomic propositions. Then we can build a truth table for several formula at once by making columns for the atomic propositions that occur in all of them. For example, let's do A -> B, B -> C, and A -> (B /\ C) all at once: alpha[A] alpha[B] alpha[C] | M[A -> B] M[A -> C] M[A -> (B /\ C)] -------------------------------------------------------------------- top top top | top top top *** top top bot | top bot bot top bot top | bot top bot top bot bot | bot bot bot bot top top | top top top *** bot top bot | top top top *** bot bot top | top top top *** bot bot bot | top top top *** VALID CONSEQUENCE ----------------- Look at the lines marked *** in the table above. M[A -> (B /\ C)] = top whenever M[A -> B] = M[A -> C] = top. We say that A -> (B /\ C) is a _valid consequence_ of {A ->B, A -> C}. We'll extend the |= notation to express that: {A -> B, A -> C} |= A -> (B /\ C) In general, we write G |= P where G is a set of formulae to indicate that every interpretation that models all of the formulae in G also models P. We express that in symbols as: G |= P if and only if for all interpretations a: if (for each Q in G: |=_a Q) then |=_a P Valid consequence expresses what we mean when we reason hypothetically ("What if ...?" kind of reasoning.) We can take set of hypotheses (propositions that we suppose are true for sake of argument), and we can ask about potential consequences. Note now that |= has three different meanings depending on how it's used! ***Theorem 1: P |= Q if and only if |= P -> Q. Proof: Consider a combined truth table for P, Q, and P -> Q. (1) Assume P |= Q. Then every model of P is a model of Q (equivalently, Q has top in the table on all the lines in which P has top). Thus by the table for implication, P -> Q must also have top in those rows. Therefore every model of P is a model of P -> Q. Further, every counterexample for P (the rows where P has bot) is a model of P -> Q. Thus every interpretation is a model for P -> Q, and so |= P -> Q. (2) Assume |= P -> Q. Then every interpretation is a model for P -> Q. Of these, consider the ones that model P. If an interpretation models P, then it must also model Q, for otherwise it would not model P -> Q. Thus Q has top on all those lines where P has top, and so P |= Q. Q.E.D. ***Theorem 2: P0, P1, ..., Pn |= Q if and only if P0, P1, ..., P_n-1 |= Pn -> Q Proof: Consider a combined truth table for P0, ..., Pn, Q, and Pn -> Q. (1) Assume P0, P1, ..., Pn |= Q. Then each interpretation that models all of P0 through Pn also models Q. Consider each interpretation that model all of P0 through P_n-1. If the interpretation also models Pn, then it models Q by assumption and therefore also Pn -> Q. If it is a counterexample for Pn, then it models Pn -> Q by the rule for implication. Thus every interpretation that models all of P0 through P_n-1 models Pn -> Q, and so P0, P1, ..., P_n-1 |= Pn -> Q. (2) Assume P0, P1, .., P_n-1 |= Pn -> Q. Then each interpretation that models all of P0 through P_n-1 also models Pn -> Q. Each one of these that also models Pn must also model Q, by the rule for implication. Therefore every interpretation that models all of P0 through Pn also models Q, and so P0, P1, ..., Pn |= Q. Q.E.D. ***Corollary: P0, P1, ..., Pn |= Q if and only if |= P0 -> (P1 -> ... -> (Pn -> Q)) Proof: Left to right: Apply Theorem 2 n times, and then apply Theorem 1. Right to left: Apply Theorem 1, then apply theorem 2 n times. Q.E.D. VERIFYING TRUTH USING PROOF --------------------------- To verify the truth of a proposition within our propositional logic, we build a truth table. Alternatively, you can run the programs you developed for homework #2; those are based on truth tables too. Either way, given a proposition, we do a bit of computation and true or false pops out with no explanation attached. The theorem statements above are propositions too (stated outside of the language of propositional logic, but that's okay). We verified their truth by constructing an "airtight" argument called a proof. The exercise of constructing the proof lends insight into *why* the proposition is true. This is valuable as long as each proof step we use "makes sense" -- if not, we may wind up at an invalid conclusion. Can we use proof to determine truth of propositions within our logical system? As it turns out we can write down a data definition whose instances represent proofs. Given one of these, a program can check that the proof actually proves the proposition in question. Moreover, a proposition is provable if and only if it is valid! That is, validity coincides with provability for the propositional logic. This is also the case for the logic on which ACL2 is based. More on this in the coming weeks!