Skip to content Skip to navigation

Connexions

You are here: Home » Content » Propositional Logic: inference rules

Navigation

Recently Viewed

This feature requires Javascript to be enabled.

Propositional Logic: inference rules

Module by: Ian Barland, John Greiner. E-mail the authors

User rating (How does the rating system work?)
Ratings

Ratings allow you to judge the quality of modules. If other users have ranked the module then its average rating is displayed below. Ratings are calculated on a scale from one star (Poor) to five stars (Excellent).

How to rate a module

Hover over the star that corresponds to the rating you wish to assign. Click on the star to add your rating. Your rating should be based on the quality of the content. You must have an account and be logged in to rate content.

:
(0 ratings)

Summary: Using inference rules (formal proofs) for determining whether a propositional formula is true.

Note: Your browser may not currently support MathML. See our browser support page for additional details. You can always view the correct math in the PDF version.

Inference

Truth tables and equivalences are useful and powerful tools, but they do not correspond to how we usually reason about things. What we will do now is look at more familiar reasoning and how to formalize that. For example, with Boolean algebra it is awkward to prove that a∧ba b implies aa. For that, it is necessary to reword the problem in terms of equivalences, as a∧b⇒a≡true a b a . Our next tool provides a more straightforward way to reason about implications.

Example 1

Given the following piece of a WaterWorld board, how would you conclude that GG is unsafe?

Figure 1: A glimpse of a WaterWorld board
Figure 1 (partIId-example.png)

Since H-has-2H-has-2, at least two of HH's three neighbors must be unsafe. But, since we know that one of these, JJ, isn't unsafe, then the two others, including GG, must both be unsafe. Let's write this out more explicitly:

Table 1
1H-has-2H-has-2would imply one of the following is true: (P-unsafeP-unsafe and G-unsafeG-unsafe), or (J-unsafeJ-unsafe and P-unsafeP-unsafe), or (G-unsafeG-unsafe and J-unsafeJ-unsafe). WaterWorld domain axiom, i.e., definition of H-has-2H-has-2
2H-has-2H-has-2 is true. Premise (by inspection of this particular board)
3One of the following is true: (P-unsafeP-unsafe and G-unsafeG-unsafe), or (J-unsafeJ-unsafe and P-unsafeP-unsafe), or (G-unsafeG-unsafe and J-unsafeJ-unsafe). lines 1,2
4not J-unsafeJ-unsafe Premise (by inspection)
5(P-unsafeP-unsafe and G-unsafeG-unsafe) lines 3,4
6G-unsafeG-unsafe line 5

Whew! A lot of small steps are involved in even this small deduction. It's apparent we'd want to automate this as much as possible! Let's look at some other short examples, which we'll formalize in a moment.

Exercise 1

How do you know that A-has-2A-has-2 proves B-unsafeB-unsafe ?

Solution

Intuitively, this is straightforward. Since A-has-2A-has-2, then both of its two neighbors, including BB, must be unsafe. For this problem, let's be a bit more formal and use WFFs instead of prose in the steps.

Table 2
1A-has-2A-has-2 Premise
2A-has-2⇒B-unsafe∧F-unsafe A-has-2 B-unsafe F-unsafe WaterWorld domain axiom, i.e., definition of A-has-2A-has-2
3B-unsafe∧F-unsafeB-unsafe F-unsafe lines 1,2
4B-unsafeB-unsafe line 3

Exercise 2

Similarly, how do you reason that A-has-1A-has-1 and G-safeG-safe prove B-unsafeB-unsafe?

Solution

Again a similar idea, if A-has-1A-has-1, then at least one of AA's two neighbors must be unsafe. But, since we know that one of these, GG isn't unsafe, then the other, BB, must be unsafe.

Table 3
1A-has-1⇒B-safe∧G-unsafe∨B-unsafe∧G-safe A-has-1 B-safe G-unsafe B-unsafe G-safe WaterWorld domain axiom
2A-has-1A-has-1 Premise
3B-safe∧G-unsafe∨B-unsafe∧G-safe B-safe G-unsafe B-unsafe G-safe lines 1,2
4G-safeG-safe Premise
5B-unsafe∧G-safeB-unsafe G-safe lines 3,4
6B-unsafeB-unsafe line 5

Formal inference rules and proofs

In the above examples, we relied on common sense to know what new true formulas could be derived from previous ones. Unfortunately, common sense is imprecise and sometimes wrong. So, we need to formalize how we form proofs.

We now define a formal proof of θθ from the premises φφ, …, ψψ, written

φ, …, ψ ⊢ θ φ, …, ψ ⊢ θ (1)
(A proof with no premises simply means there is nothing on the left of the turnstile: ⊢ θ⊢ θ.) For example, we'll show shortly that H-has-2 ⊢ G-unsafeH-has-2 ⊢ G-unsafe. A proof consists of a sequence of WFFs, each with a justification for its truth. We will describe four permissible justifications for each step:
  • A premise.
  • An axiom.
  • An inference rule.
  • A subproof.

Aside:

Officially we might want to annotate the turnstile with “ww”, to mean “proves within the WaterWorld inference system”, indicating our use of the WaterWorld domain axioms. If you're proving things about other domains, you'd use different domain axioms.

Example 2

We can formalize the above examples to show each of the following:

  • H-has-2 ⊢ G-unsafeH-has-2 ⊢ G-unsafe
  • A-has-2 ⊢ B-unsafeA-has-2 ⊢ B-unsafe
  • A-has-1, G-safe ⊢ B-unsafeA-has-1, G-safe ⊢ B-unsafe
See below for formal proofs of some of these.

Stating an axiom, a simple assumed truth, is a rather trivial, boring way of coming up with a true formula. Some axioms are domain axioms: they pertain only to the domain you are considering, such as WaterWorld. In our case, we don't have any axioms that aren't domain axioms. If our domain were arithmetic, our axioms would describe how multiplication distributes over addition, etc.

Just using axioms is not enough, however. The interesting part is to deduce new true formulas from axioms and the results of previous deductions.

Note:

“The point of philosophy is to start with something so simple as not to seem worth stating, and to end with something so paradoxical that no one will believe it.” Bertrand Russell, The Philosophy of Logical Atomism
An inference rule formalizes what steps are allowed in proofs. We'll use this list of valid inference rules as our definition, but, this is just one set of possible inference rules, and other people could use slightly different ones.

First, let's look at some simple examples, using the simpler inference rules.

Example 3

We'll formalize a previous exercise to show A-has-2 ⊢ B-unsafeA-has-2 ⊢ B-unsafe.

Table 4
1A-has-2A-has-2 Premise
2A-has-2⇒B-unsafe∧F-unsafe A-has-2 B-unsafe F-unsafe WaterWorld domain axiom
3B-unsafe∧F-unsafe B-unsafe F-unsafe ⇒⇒Elim, lines 1,2, where φ=A-has-2φ A-has-2, and ψ=B-unsafe∧F-unsafe ψ B-unsafe F-unsafe
4B-unsafeB-unsafe ∧∧Elim (left), line 3, where φ=B-unsafeφ B-unsafe, and ψ=F-unsafeψ F-unsafe

What we mean in line 3, for example, is that we are using the domain axiom ⇒⇒Elim. That states that if we know φ⇒ψφ ψ, and we know φφ, then we can conclude ψψ. In line 3, we have defined φ=A-has-2φ A-has-2 and ψ=B-unsafe∧F-unsafe ψ B-unsafe F-unsafe , so that φ⇒ψφ ψ corresponds to the conclusion of line 2 and φφ corresponds to that of line 1. Thus, this domain axiom applies, and we get the conclusion ψψ.

That's almost exactly like the steps we took in the previous informal proof, but now we're a bit pickier about our justifications for each step.

Formally, when using a domain axiom, the justification is a combination of the name of that inference rule, the line numbers of which previous WFFs are being used, and a description of how those WFFs are used in that inference rule in this particular step. Later, we'll often omit the description of exactly how the specific inference rule is used, since in many cases, that information is painfully obvious.

Example 4

In this system, commutativity of ∧∧ and ∨∨ are not among the inference rules. However, they do follow. For example, consider the following proof of A∧B ⊢ B∧AA B ⊢ B A.

Table 5
1A∧BA B Premise
2AA ∧∧Elim (left), line 1, where φ=Aφ A
3BB ∧∧Elim (right), line 1, where ψ=Bψ B
4B∧AB A ∧∧Intro, lines 3,2, where φ=Bφ B, and ψ=Aψ A

Does this example also show that C∧D ⊢ D∧CC D ⊢ D C? Well, yes and no. That proof does not have anything to do with propositions CC and DD. But, clearly, we could create another nearly identical proof for C∧D ⊢ D∧CC D ⊢ D C, by substituting CC and DD for AA and BB, respectively. What about proving the other direction of commutativity: B∧A ⊢ A∧BB A ⊢ A B? Once again, the proof has exactly the same form, but substituting BB and AA for AA and BB, respectively. Stating such similar proofs over and over is technically necessary, but not very interesting. Instead, when the proof depends solely on the form of the formula and not on any axioms, we'll use meta-variables to generalize.

Example 5

Generalized ∧∧ commutativity: χ∧υ ⊢ υ∧χχ υ ⊢ υ χ

Table 6
1χ∧υχ υ Premise
2υυ ∧∧Elim (left), line 1, where φ=χφ χ
3χχ ∧∧Elim (right), line 1, where ψ=υψ υ
4υ∧χυ χ ∧∧Intro, lines 3,2, where φ=υφ υ, and ψ=χψ χ

Exercise 3

Similarly, associativity of ∧∧ and ∨∨ are not among the inference rules. This is a particularly important detail, since our WaterWorld domain axioms frequently use formulas of the form a∧b∧ca b c, which isn't technically legal according to our definition of WFFs. What we'd like to show is that χ∧υ∧ω ⊢ χ∧υ∧ω χ υ ω ⊢ χ υ ω and χ∧υ∧ω ⊢ χ∧υ∧ω χ υ ω ⊢ χ υ ω as well as the equivalent for ∨∨. Thus, when we see three, four, or more terms in a conjunction (or disjunction), we can legitimately group them as we see fit.

Solution

Here, we'll show only χ∧υ∧ω ⊢ χ∧υ∧ω χ υ ω ⊢ χ υ ω and leave the other direction (and ∨∨'s associativity) to the reader. These are all very similar to the previous commutativity example.

Table 7
1χ∧υ∧ωχ υ ω Premise
2χ∧υχ υ ∧∧Elim (left), line 1
3χχ ∧∧Elim (left), line 2
4υυ ∧∧Elim (right), line 2
5ωω ∧∧Elim (right), line 1
6υ∧ωυ ω ∧∧Intro, lines 4,5
7χ∧υ∧ωχ υ ω ∧∧Intro, lines 3,6

Note that we omitted the detailed explanation of how each rule applies, since this should be clear in each of these steps.

These deductions are straightforward and should be unsurprising, but perhaps not too interesting. These simple rules can carry us far and will be used commonly in other examples.

Example 6

The case-elimination rule is easy enough for a dog! Rico has a vocabulary of over 200 words, and if asked to fetch an unknown toy, he can pick it out of a group of known toys by process-of-elimination. (It's almost enough to make you wonder whether dogs know calculus.)

Figure 2: This Border Collie knows his inference rules.
Figure 2 (ricodog.jpg)

There is a subtle difference between implication (⇒⇒) and provability (⊢). Both embody the idea that the truth of the right-hand-side follows from the left-hand-side. But, ⇒⇒ is a syntactic formula connective combining two WFFs into a larger WFF, while ⊢ combines a list of propositions and a WFF into a statement about provability.

Exercise 4

Show that, φ ⊢ ψφ ⊢ ψ is equivalent to ⊢ φ⇒ψ⊢ φ ψ in that, we can show one if and only if we can show the other.

Solution

First, if we know φ ⊢ ψφ ⊢ ψ, then that means there is some written proof… we know ⊢ φ⇒ψ⊢ φ ψ, simply by ⇒⇒Intro.

If we know ⊢ φ⇒ψ⊢ φ ψ, then if we add a premise φφ, then ψψ follows by ⇒⇒Elim.

Note how this proof is about other proofs! (However, while we reason about this particular inference system, we're not using this system while proving things about it — this proof is necessarily outside the inference system.

Content actions

Give Feedback:

E-mail the module authors | Rate module ( How does the rating system work?)

Rating system

Ratings

Ratings allow you to judge the quality of modules. If other users have ranked the module then its average rating is displayed below. Ratings are calculated on a scale from one star (Poor) to five stars (Excellent).

How to rate a module

Hover over the star that corresponds to the rating you wish to assign. Click on the star to add your rating. Your rating should be based on the quality of the content. You must have an account and be logged in to rate content.

(0 ratings)

Download:

Module PDF

Add module to:

My Favorites (?)

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

| A lens (?)

Definition of a lens

Lenses

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

What is in a lens?

Lens makers point to Connexions 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 Connexions 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