Skip to content Skip to navigation

OpenStax-CNX

You are here: Home » Content » Propositional Logic: formulas

Navigation

Lenses

What is a lens?

Definition of a lens

Lenses

A lens is a custom view of the content in the repository. You can think of it as a fancy kind of list that will let you see content through the eyes of organizations and people you trust.

What is in a lens?

Lens makers point to materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

Who can create a lens?

Any individual member, a community, or a respected organization.

What are tags? tag icon

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

This content is ...

Affiliated with (What does "Affiliated with" mean?)

This content is either by members of the organizations listed or about topics related to the organizations listed. Click each link to see a list of all content affiliated with the organization.
  • Rice Digital Scholarship

    This module is included in aLens by: Digital Scholarship at Rice UniversityAs a part of collection: "Intro to Logic"

    Click the "Rice Digital Scholarship" link to see all content affiliated with them.

Recently Viewed

This feature requires Javascript to be enabled.
 

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

¬ca¬c c a c , or equivalently, ¬c a¬c c a c

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

Example

¬ca¬cb 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: abc ab c a b c a b c , whereas ⇒ groups right-to-left.

Example 1

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

¬((¬ac(bac))¬(a¬b)) a c b a c a 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 abab. Similarly, aa, bb, and cc are meta-variables to be replaced with a proposition, such as bb.

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

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-solnis-soln, include-solnsinclude-solns, is-practiceis-practice), respectively. The if's condition boils down to the WFF is-soln¬(include-solnsis-practice) 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, 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-unsafeA-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 aab a a b , one possible truth assignment is a=truea and b=falseb . With that truth assignment, the formula is false.

Aside:

We've used three different symbols to describe “equality” in some sense:

  • ab a b is a formula. The symbol “⇔” is a logical connective.
  • φψ φ ψ is a statement that two formulas are equivalent that is, the same for all truth assignments.
  • a=truea defines the value of a proposition. We also use the symbol for defining variables, b=ψb ψ, and meta-variables, φ=ψφ ψ.
Of these, only “⇔” occurs within a formula.

Commonly, people use symbols such as “≡” for multiple purposes. This is problematic when part of what we are studying are the syntactic formulas themselves.

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

Example

A-unsafeA-unsafe A-unsafe A-unsafe

Example

aab a a b

Definition 4: unsatisfiable
A WFF which is false under any truth assignment.

Example

¬(A-unsafeA-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 x20 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
Figure 1 (jackvenn.png)

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.)

Exercise 1

“ Pitching always beats batting and vice-versa. ”

Solution

Unsatisfiable.

Exercise 2

You can observe a lot just by watchin'.

Solution

Tautology, arguably.

Exercise 3

Nobody goes there anymore… it's too crowded.

Solution

Unsatisfiable, unless of course you interpret “nobody” as “nobody of note”.

Exercise 4

It sure gets late early out here.

Solution

Neither. If you interpret “gets late” as a social issue but “early” as a clock issue, then the statement might be true, depending on where “here” is.

Exercise 5

Always go to other people's funerals; otherwise they won't come to yours.

Solution

Unsatisfiable, except perhaps in a karmic sense.

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:

  • TAUTOLOGY: given a formula φφ, is it a tautology?
  • SATisfiability: Give a formula φφ, is it satisfiable? (Is there some truth assignment to its variables, that makes it true?)
  • EQUIV: Given two WFFs φφ and ψψ, are they equivalent? (Do they give the same result for all possible truth assignments to their variables?

Game-specific rules

Is xyzx y z a tautology? Clearly not. Setting the three propositions each to false, the formula is false. But now consider: Is A-has-0A-has-1A-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-has-0B-safeG-safe A-has-0 B-safe G-safe
  • A-has-2B-unsafeG-unsafe A-has-2 B-unsafe G-unsafe

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

Content actions

Download module as:

Add module to:

My Favorites (?)

'My Favorites' is a special kind of lens which you can use to bookmark modules and collections. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need an account to use 'My Favorites'.

| A lens I own (?)

Definition of a lens

Lenses

A lens is a custom view of the content in the repository. You can think of it as a fancy kind of list that will let you see content through the eyes of organizations and people you trust.

What is in a lens?

Lens makers point to materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

Who can create a lens?

Any individual member, a community, or a respected organization.

What are tags? tag icon

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

| External bookmarks