Well-Formed Formulas

If we want to develop complicated expressions about breakfast foods like eggs, hashbrowns, and so on, we will want an exact grammar telling us how to connect the propositions, what connections are allowed, and when parentheses are necessary (if at all). We will choose a grammar so that all our formulas are fully parenthesized:

Definition 1: Well-Formed formula (WFF)

1. A constant: true or false. (If you prefer brevity, you can write “T” or “F”.)

2. A propositional variable.

Example

aa

3. A negation ¬φφ, where φφ is a WFF.

Example

¬cc

4. A conjunction φ∧ψφ ψ, where φφ and ψψ are WFFs.

Example

a∧¬ca c

5. A disjunction φ∨ψφ ψ, where φφ and ψψ are WFFs.

Example

¬c∨a∧¬c c a c , or equivalently, ¬c ∨ a∧¬c c a c

6. An implication φ⇒ψφ ψ, where φφ and ψψ are WFFs.

Example

¬c∨a∧¬c⇒b c a c b , or equivalently, ¬c ∨ a∧¬c ⇒b c a c b

The last two examples illustrate that we can add parentheses to formulas to make the precedence explicit. While some parentheses may be unnecessary, over-parenthesizing often improves clarity. We introduced the basic connectives in the order of their precedence: ¬ has the highest precedence, while ⇒ has the lowest. Furthermore, ∧ and ∨ group left-to-right: a∧b∧c≡ a∧b ∧c a b c a b c , whereas ⇒ groups right-to-left.

Variations of well-formed formulas occur routinely in writing programs. While different languages might vary in details of what connectives are allowed, how to express them, and whether or not all parentheses are required, all languages use WFFs.

;; is-a-solution?: paragraph -> boolean
;; A function to tell if we are looking at a "solution" paragraph.
;; Assume this is provided.

;; is-in-a-practice-prob?: paragraph -> boolean
;; A function to tell if Is the current problem a practice problem?
;; Assume this is provided.

;; include-all-solutions?: boolean
;; A variable for the entire file.
;; Assume this is provided.


;; show-or-hide-soln: paragraph -> paragraph
;; Either return the given paragraph,
;; or (if it shouldn't be revealed) return a string saying so.
;;
(define (show-or-hide-soln a-para)
   (if (and (is-a-solution? a-para)
            (not (or include-all-solns? (is-in-a-practice-prob? a-para)))
       "(see solution set)"
       a-para))

Keep in mind that a WFF is purely a syntactic entity. We'll introduce rules later for re-writing or reasoning with WFFs, but it's those rules that will be contrived to preserve our meaning of connectives like ∧ or ¬. The truth value of a WFF depends on the truth values we assign to the propositions it involves.

When writing a program about WFFs, verifying syntactic property, calculating a value, counting the number of negations or bbs, etc., such programs exactly follow the definition of WFF given.

Some formulas are truer than others

Is the formula A-unsafe∨A-has-2A-unsafe A-has-2 true? Your response should be that it depends on the particular board in question. But some formulas are true regardless of the board. For instance, A-unsafe∨¬A-unsafeA-unsafe A-unsafe: this holds no matter what. Similarly, A-unsafe∧¬A-unsafeA-unsafe A-unsafe can never be satisfied (made true), no matter how you try to set the variable A-unsafeA-unsafe.

Definition 2: truth assignment

An assignment of a value true or false to each proposition being used.

Example

For the formula a⇒a∧b a a b , one possible truth assignment is a=truea and b=falseb . With that truth assignment, the formula is false.

Definition 3: tautology

A WFF which is true under any truth assignment (any way of assigning true/false to the propositions).

Example

A-unsafe⇒A-unsafe A-unsafe A-unsafe

Example

a⇒a∨b a a b

Definition 4: unsatisfiable

A WFF which is false under any truth assignment.

Example

¬A-unsafe⇒A-unsafe A-unsafe A-unsafe

Example

a⇒¬a a a

Note that in algebra, there are certainly formulas which are true (or similarly, false) for all values, but they don't get special names. For example, over the real numbers, any assignment to xx makes the formula x2≥0 x2 0 true, so it's similar to a tautology. Similarly, x=x+1 x x1 is unsatisfiable, since it can't be made true for any assignment to xx.

Some people use the term contingency to mean formulas in between: things which can be either true or false, depending on the truth assignment. Really, tautologies and unsatisfiable formulas are boring. However, trying to determine whether or not a formula is a tautology (or, unsatisfiable) is of interest. That's what proofs are all about!

Figure 1: Kinds of formulas: tautologies, contingencies, unsatisfiables

Identify the following Yogi Berra quotes either as tautologies, unsatisfiable, or neither. (Take these exercises with a grain of salt, since the English statements are open to some interpretation.)

Finding Truth

Now that we've seen how to express concepts as precise formulas; we would like to reason with them. By “reason”, we mean some automated way of ascertaining or verifying statements —— some procedure that can be carried out on an unthinking computer that can only push around symbols. In particular, for propositional logic, we'll restrict our attention to some (closely related) problems:

Game-specific rules

Is x∨y∨zx y z a tautology? Clearly not. Setting the three propositions each to false, the formula is false. But now consider: Is A-has-0∨A-has-1∨A-has-2A-has-0 A-has-1 A-has-2 a tautology? The answer here is “ yes of course, … well, as long we're interpreting those propositions to refer to a WaterWorld board. ” We'll capture this notion by listing a bunch of domain axioms for WaterWorld: formulas which are true for all WaterWorld boards.

There are a myriad of domain axioms which express the rules of WaterWorld. Here are a few of them:

A more complete list is here. Whenever we deal with WaterWorld, we implicitly take all these domain axioms as given.