# Connexions

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?

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

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

Inside Collection (Course):

# 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?

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:

 1 H-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 2 H-has-2H-has-2 is true. Premise (by inspection of this particular board) 3 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). lines 1,2 4 not J-unsafeJ-unsafe Premise (by inspection) 5 (P-unsafeP-unsafe and G-unsafeG-unsafe) lines 3,4 6 G-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 ?

### Exercise 2

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

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

 1 A-has-2A-has-2 Premise 2 A-has-2⇒B-unsafe∧F-unsafe A-has-2 B-unsafe F-unsafe WaterWorld domain axiom 3 B-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 4 B-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.

 1 A∧BA B Premise 2 AA ∧∧Elim (left), line 1, where φ=Aφ A 3 BB ∧∧Elim (right), line 1, where ψ=Bψ B 4 B∧AB 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: χυ υχχ υ υ χ

 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.

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

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.

## Content actions

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

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

### 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?

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?

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

### Reuse / Edit:

Reuse or edit collection (?)

#### Check out and edit

If you have permission to edit this content, using the "Reuse / Edit" action will allow you to check the content out into your Personal Workspace or a shared Workgroup and then make your edits.

#### Derive a copy

If you don't have permission to edit the content, you can still use "Reuse / Edit" to adapt the content by creating a derived copy of it and then editing and publishing the copy.

| Reuse or edit module (?)

#### Check out and edit

If you have permission to edit this content, using the "Reuse / Edit" action will allow you to check the content out into your Personal Workspace or a shared Workgroup and then make your edits.

#### Derive a copy

If you don't have permission to edit the content, you can still use "Reuse / Edit" to adapt the content by creating a derived copy of it and then editing and publishing the copy.