Lecture 3: Propositional Logic in Code

1 Purpose

Review propositional logic, how it can be expressed in code.

2 Outline

Who can tell me something they remember from propositional logic?

Variables and logical operators. Variables can be assigned True or False.

Variables combined with operators into formulas. Formulas can be some combination of:

1. Satisfiable (there exists some assignment of variables that makes the formula True)

2. Valid, or Tautologies (for all assignments of variables, the formula is True)

3. Falsifiable (there exists some assignment of variables that makes the formula False)

4. Unsatisfiable (for all assignments, the formula is False)

What are some operators?

AND, OR, NOT, XOR, IMPLIES, ITE

We can describe operators, and formulas in general, via truth tables.

Here is AND (usually written \land).

Let’s write down OR, NOT, IMPLIES, and ITE.

We can also write truth tables for larger expressions: for every variable, we need to consider the two possible assignments (True or False), so for N variables, 2^N rows of the table.

Once we’ve filled in the variable columns, the columns for the formula (and, if we want to do subformulas first, we can), are calculated based on the values that already exist in the row.

This is review: perhaps recent, if you just took Discrete, perhaps rusty, if you took it a while ago. But here’s where we diverge. Rather than writing logical formulas on paper, we want to express them in code.

How? Well, there’s always a question as to how you best model something in data, but here, we have most of the tools already with booleans values and boolean operators.

Let’s figure out equivalents to a few operators.

Now, we can also write down formulas as definitions. For example:

(define (p1 P Q R)
  (or P (and Q R)))

(define (p3 P Q)
  (and (or P Q) (or P (not Q))))

(define (p4 P Q)
  (boolean=? (boolean=? P Q) (and (or P (not Q)) (or (not P) Q))))

On its own, this is fine, but perhaps hasn’t gotten us very far: the statements in math were already quite precise, if anything, we’ve only made them a bit more verbose. Of course, perhaps having the ability to define named sub-parts is useful, but it’s not hard to imagine defining notation to do that in the math notation.

What really changes things is when we translate our truth tables: our proofs. Because while I can write, on paper, the following truth table:

Now, did I get that truth table correct? I might have. I was pretty careful about it. But even just this formula with two variables already had me doing twelve calculations, any one of which might have been wrong, and there is nothing that checked it. We can, and should, do better. How?

By turning our truth tables, which are proofs, into code that runs:

(define (p5 P Q)
  (and (or P Q) (or P (not Q))))

(check-expect (p5 #t #t) #t)
(check-expect (p5 #t #f) #t)
(check-expect (p5 #f #t) #f)
(check-expect (p5 #f #f) #f)

Note a couple things. First, while we certainly could make the intermediate formulas as definitions, and define truth tables for them, we don’t need to, especially since they are partly a way of checking your work, and here our work will be checked by the evaluation of ISL-Spec.

Defining operators Above, we simply speculated that and corresponds to \land, or to \lor, and so on. But we can also check this, via truth tables.

(check-expect (and #t #t) #t)
(check-expect (and #t #f) #f)
(check-expect (and #f #t) #f)
(check-expect (and #f #f) #f)

(check-expect (or #t #t) #t)
(check-expect (or #t #f) #t)
(check-expect (or #f #t) #t)
(check-expect (or #f #f) #f)

That might seem pretty obvious, but some operators from logic don’t correspond to built in operators that we already understand. For example, logical implication and exclusive or. But we can define them in terms of other operators. For example, a well-known encoding of logical implication uses \land and \neg, and we can construct exclusive or in terms of \land, \lor, and \neg. Looking at these definitions, especially the first one, you may wonder if they actually correspond to the operators we want. But we can check them using truth tables.

Some may have many different implementations: we don’t have to understand them, as we can validate them against their truth table.

(define implies (lambda (P Q) (not (and P (not Q)))))
(check-expect (implies #t #t) #t)
(check-expect (implies #t #f) #f)
(check-expect (implies #f #t) #t)
(check-expect (implies #f #f) #t)


(define (xor P Q)
  (not (or (and P Q)
           (not (or P Q)))))
(check-expect (xor #t #t) #f)
(check-expect (xor #t #f) #t)
(check-expect (xor #f #t) #t)
(check-expect (xor #f #f) #f)

(define (xor1 P Q)
  (or (and P (not Q))
      (and (not P) Q)))
(check-expect (xor1 #t #t) #f)
(check-expect (xor1 #t #f) #t)
(check-expect (xor1 #f #t) #t)
(check-expect (xor1 #f #f) #f)

(define (xor2 P Q)
  (not (equal? P Q)))
(check-expect (xor2 #t #t) #f)
(check-expect (xor2 #t #f) #t)
(check-expect (xor2 #f #t) #t)
(check-expect (xor2 #f #f) #f)

(define (xor3 P Q)
  (and (or P Q)
       (not (and P Q))))
(check-expect (xor3 #t #t) #f)
(check-expect (xor3 #t #f) #t)
(check-expect (xor3 #f #t) #t)
(check-expect (xor3 #f #f) #f)

We can also, of course, define formulas using these derived operators.

(define (p2 P)
  (implies P (not P)))

Simplification Equality in propositional logic is definable, and can be validated via truth tables. If an equality is always true, so it is a tautology (or valid), then the two formulas are equivalent. For example:

(define (p8 P Q)
  (boolean=? (and P Q)
             (and Q P)))
(check-expect (p8 #t #t) #t)
(check-expect (p8 #t #f) #t)
(check-expect (p8 #f #t) #t)
(check-expect (p8 #f #f) #t)

Your equivalence could also be a simplification. In homework, you are asked to simplify, and while we do not ask you to prove your simplifications in this way, you certainly can if you wish to check your work.

(define (p9 P Q R)
  (boolean=? (and P Q (or R (not R)))
             (and Q P)))
(check-expect (p9 #t #t #t) #t)
(check-expect (p9 #t #f #t) #t)
(check-expect (p9 #f #t #t) #t)
(check-expect (p9 #f #f #t) #t)

(check-expect (p9 #t #t #f) #t)
(check-expect (p9 #t #f #f) #t)
(check-expect (p9 #f #t #f) #t)
(check-expect (p9 #f #f #f) #t)