Skip to content Skip to navigation Skip to collection information

OpenStax-CNX

You are here: Home » Content » Intro to Logic » propositional inference rules

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 collection is included in aLens by: Digital Scholarship at Rice University

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

Recently Viewed

This feature requires Javascript to be enabled.
 

propositional inference rules

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

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

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 aba b implies aa. For that, it is necessary to reword the problem in terms of equivalences, as abatrue 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-2B-unsafeF-unsafe A-has-2 B-unsafe F-unsafe WaterWorld domain axiom, i.e., definition of A-has-2A-has-2
3B-unsafeF-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-1B-safeG-unsafeB-unsafeG-safe A-has-1 B-safe G-unsafe B-unsafe G-safe WaterWorld domain axiom
2A-has-1A-has-1 Premise
3B-safeG-unsafeB-unsafeG-safe B-safe G-unsafe B-unsafe G-safe lines 1,2
4G-safeG-safe Premise
5B-unsafeG-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-2B-unsafeF-unsafe A-has-2 B-unsafe F-unsafe WaterWorld domain axiom
3B-unsafeF-unsafe B-unsafe F-unsafe Elim, lines 1,2, where φ=A-has-2φ A-has-2, and ψ=B-unsafeF-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-unsafeF-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 AB BAA B B A.

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

Does this example also show that CD DCC 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 CD DCC D D C, by substituting CC and DD for AA and BB, respectively. What about proving the other direction of commutativity: BA ABB 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 abca 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.

Collection Navigation

Content actions

Download:

Collection as:

PDF | EPUB (?)

What is an EPUB file?

EPUB is an electronic book format that can be read on a variety of mobile devices.

Downloading to a reading device

For detailed instructions on how to download this content's EPUB to your specific device, click the "(?)" link.

| More downloads ...

Module as:

PDF | More downloads ...

Add:

Collection 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

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