您在這裡

Well-Formed Formulas

15 六月, 2015 - 15:50
Available under Creative Commons-ShareAlike 4.0 International License. Download for free at http://cnx.org/contents/383d4b87-2d7b-454e-99fe-2eaa43eae8ff@20.20

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)

  1. A constant: true or false. (If you prefer brevity, you can write "T" or "F".)
  2. A propositional variable.

Example

a

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

Example

¬c

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

Example

a¬c

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

Example

¬ca¬c, or equivalently, (¬c) ∨ (a¬c)

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

Example

¬ca¬cb, 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: abc ≡ (ab) ∧ c, whereas ⇒ groups right-to-left.

Example 2.2

We can combine these ways of forming WFFs in arbitrarily complex ways, for example,

\dashv ((\dashv a\wedge c\vee (b\Rightarrow a\Rightarrow c))\wedge \dashv (a\Rightarrow \dashv b))
While large WFFs are common, and we will use some, ones with this much nesting are not.

Note: φ, ψ, and θ are meta-variables standing for any WFF. The literal character "φ" doesn't actually show up inside some WFF; but instead, any particular formula can be used where we write "φ". It is a variable which you the reader must substitute with some particular WFF, such as " ab ". Similarly, a, b, and c are meta-variables to be replaced with a proposition, such as "b".

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.