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 2.5: Well-Formed formula (WFF)
- A constant: true or false. (If you prefer brevity, you can write "T" or "F".)
- A propositional variable.
Example
a
- A negation ¬φ, where φ is a WFF.
Example
¬c
- A conjunction φ ∧ ψ, where φ and ψ are WFFs.
Example
a ∧¬c
- A disjunction φ ∨ ψ, where φ and ψ are WFFs.
Example
¬c ∨ a ∧¬c, or equivalently, (¬c) ∨ (a ∧¬c)
- An implication φ ⇒ ψ, where φ and ψ are WFFs.
Example
¬c ∨ a ∧¬c ⇒ b, or equivalently, ((¬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, whereas ⇒ groups right-to-left.
Example 2.2
We can combine these ways of forming WFFs in arbitrarily complex ways, for example,
While large WFFs are common, and we will use some, ones with this much nesting are not.
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.
Example 2.3
When creating the homeworks' web pages, the authors keep the problems and solutions together in one file. Then, a program reads that file, and creates a new one which either excludes the solution (for the problem set), or includes it (for the solution set, and for practice-problems). The condition for deciding whether to include the solutions is a WFF.
;; 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))
Note that the Boolean variable include-all-solutions? and Boolean values of (is-a-solution? a-para) and (is-in-a-practice-prob? a-para) play the part of propositions (is − soln, include − solns, is − practice), respectively. The if's condition boils down to the WFF is − soln ∧ ¬ (include − solns ∨ is − practice).
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, veriflying syntactic property, calculating a value, counting the number of negations or bs, etc., such programs exactly follow the definition of WFF given.
- 5983 reads
