Skip to content Skip to navigation Skip to collection information

Connexions

You are here: Home » Content » Intro to Logic » Exercises for Propositional Logic II

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.
 

Exercises for Propositional Logic II

Module by: Ian Barland, John Greiner, Phokion Kolaitis, Moshe Vardi, Matthias Felleisen. E-mail the authors

Reasoning with Inference Rules

For proofs on this homework, remember that each step must be justified by one of the following:

  • a premise,
  • a WaterWorld axioms,
  • a listed inference rule with the referenced line numbers (and, if ambiguous, substitutions for the inference rule's meta-variables), or
  • a subproof shown inline, or equivalently, a theorem/lemma shown previously.
Except where otherwise directed, you may use any theorem shown in the text or by a previous exercise, even if that exercise was not assigned.

Exercise 1

Fill in the blank reasons in the following proof that ∨ commutes, that is, χ∨υ ⊢ υ∨χχ υ ⊢ υ χ.

Table 1
1χ∨υχ υ  Premise
2subproof:χ ⊢ υ∨χχ ⊢ υ χ  
2.a  χχ Premise for subproof
2.b  υ∨χυ χ ∨Intro, line 2.a
3subproof:υ ⊢ υ∨χυ ⊢ υ χ  
3.a  υυ Premise for subproof
3.b  υ∨χυ χ ____________________
4υ∨χυ χ  ____________________

Exercise 2

Show that φ∧ψ, φ⇒θ, ψ⇒δ ⊢ θ∧δφ ψ, φ θ, ψ δ ⊢ θ δ.

Note:

It should take around 8 steps.

Exercise 3

Show what is often called the implication chain rule: φ⇒ψ, ψ⇒θ ⊢ φ⇒θφ ψ, ψ θ ⊢ φ θ.

Exercise 4

[Practice problem——solution provided.]

Show what is often called negated-or-elimination (left): ¬(φ∨ψ) ⊢ ¬φφ ψ ⊢ φ.

Note:

Think backwards. How can we end with ¬φφ? One way is to end with RAA, under the premise φφ. Using that premise φφ and the starting premise ¬(φ∨ψ)φ ψ can you derive the contradiction?

Solution

Table 2
1¬(φ∨ψ)φ ψ  Premise
2subproof:φ ⊢ falseφ ⊢   
2.a  φφ Premise for subproof
2.b  φ∨ψφ ψ ∨Intro, line 2a
2.c  false falseIntro, lines 1,2b
3¬φφ  RAA, line 2

Exercise 5

Using the inference rule RAA, prove ¬φ ⊢ ¬(φ∧ψ)φ ⊢ φ ψ.

Exercise 6

Show that ¬W-safe∨¬Y-unsafe ⊢ W-unsafe∨Y-safe W-safe Y-unsafe ⊢ W-unsafe Y-safe.

Note:

The proof is a bit longer than you might expect. Use the ∨Elim inference rule to get the final result.

Exercise 7

In our inference rules, unlike our equivalences, we chose to not include any corresponding to distributivity.

  1. Prove a left-hand version of one direction of distributivity: φ∧(ψ∨θ) ⊢ φ∧ψ∨φ∧θ φ ψθ ⊢ φ ψ φ θ .

  2. Use the previous part's result, plus ∧'s commutativity to prove the corresponding right-hand version: (ψ∨θ)∧φ ⊢ ψ∧φ∨θ∧φ ψθ φ ⊢ ψ φ θ φ .

Exercise 8

In our inference rules, unlike our equivalences, we chose to not include any corresponding to DeMorgan's Law. Show that each of the following versions is still provable.

  1. φ∨ψ ⊢ ¬(¬φ∧¬ψ)φ ψ ⊢ φ ψ
  2. ¬(φ∨ψ) ⊢ ¬φ∧¬ψφ ψ ⊢ φ ψ
  3. φ∧ψ ⊢ ¬(¬φ∨¬ψ)φ ψ ⊢ φ ψ
  4. ¬(φ∧ψ) ⊢ ¬φ∨¬ψφ ψ ⊢ φ ψ

Exercise 9

The above exercise suggests that it would be useful to have an inference rule or theorem that says given θ ⊢ ¬δθ ⊢ δ, then ¬θ ⊢ δθ ⊢ δ. Or, equivalently, because of ⇒Intro and ⇒Elim, θ⇒¬δ ⊢ ¬θ⇒δθ δ ⊢ θ δ. Why don't we?

Exercise 10

In our inference rules, unlike our equivalences, we have nothing that directly equates φ⇒ψφ ψ and ¬φ∨ψφ ψ. Prove each of the following.

  1. φ⇒ψ ⊢ ¬φ∨ψφ ψ ⊢ φ ψ
  2. ¬φ∨ψ ⊢ φ⇒ψφ ψ ⊢ φ ψ

Exercise 11

Prove the following: φ⇒ψ, ψ⇒φ ⊢ φ∧ψ∨¬φ∧¬ψφ ψ, ψ φ ⊢ φ ψ φ ψ

Exercise 12

Prove what is commonly called the Law of Excluded Middle: ⊢ χ∨¬χ⊢ χ χ.

  1. Give a short proof citing our previous proof of ⊢ ¬(χ∧¬χ)⊢ χ χ and the relevant version of DeMorgan's Law from above.

  2. Give a direct version without using previous theorems.

    Note:

    Use RAA two or three times.

Exercise 13

Prove the missing steps and reasons in the following WaterWorld proof of X-has-1 ⊢ W-unsafe∨Y-unsafeX-has-1 ⊢ W-unsafe Y-unsafe.

Table 3
1X-has-1X-has-1  ____________________
2____________________  WaterWorld axiom
3____________________  ⇒Elim, lines 1,2
4subproof:W-safe∧Y-unsafe ⊢ W-unsafe∨Y-unsafe W-safe Y-unsafe ⊢ W-unsafe Y-unsafe  
4.a  W-safe∧Y-unsafe W-safe Y-unsafe Premise for subproof
4.b  Y-unsafeY-unsafe ____________________
4.c  W-unsafe∨Y-unsafeW-unsafe Y-unsafe ____________________
5subproof:¬(W-safe∧Y-unsafe) ⊢ W-unsafe∨Y-unsafe W-safe Y-unsafe ⊢ W-unsafe Y-unsafe  
5.a  ¬(W-safe∧Y-unsafe) W-safe Y-unsafe Premise for subproof
5.b  W-unsafe∧Y-safeW-unsafe Y-safe CaseElim (left), lines ____________________ where φ=____________________φ ____________________, and ψ=____________________ψ ____________________
5.c  ____________________ ____________________
5.d  W-unsafe∨Y-unsafeW-unsafe Y-unsafe ____________________
6W-safe∧Y-unsafe∨¬(W-safe∧Y-unsafe) W-safe Y-unsafe W-safe Y-unsafe   Theorem: Excluded Middle, where χ=____________________ χ ____________________
7W-unsafe∨Y-unsafeW-unsafeY-unsafe  ____________________

Exercise 14

[Practice problem——solution provided.]

Figure 1: A sample WaterWorld board
Figure 1 (hwA-1.png)

Given the above figure, and using any of the immediately obvious facts as premises, prove that location PP is safe by using our proof system and the WaterWorld axioms.

While this proof is longer (over two dozen steps), it's not too bad when sub-proofs are used appropriately. To make life easier, you may use the following theorem: Q-has-1⇒P-safe∧R-safe∨P-safe∧W-safe∨R-safe∧W-safe Q-has-1 P-safe R-safe P-safe W-safe R-safe W-safe , along with any proven previously. When looking at the given board, you can use premises like Y-safeY-safe as well as ¬Y-unsafeY-unsafe.

Solution

Table 4
1Q-has-1Q-has-1  Premise
2X-has-1X-has-1  Premise
3¬Y-unsafeY-unsafe  Premise
4W-unsafe∨Y-unsafeW-unsafe Y-unsafe  Theorem: above problem, line 2
5Y-unsafe∨W-unsafeY-unsafe W-unsafe  Theorem: ∨ commutes, line 4
6W-unsafeW-unsafe  CaseElim, lines 3,5
7subproof:¬¬(P-safe∧W-safe) ⊢ falseP-safe W-safe ⊢   
7.a  ¬¬(P-safe∧W-safe)P-safe W-safe Premise for subproof
7.b  P-safe∧W-safeP-safe W-safe ¬Elim, line 7.a
7.c  W-safeW-safe ∧Elim, line 7.b
7.d  W-safe⇒¬W-unsafeW-safe W-unsafe WaterWorld axiom
7.e  ¬W-unsafeW-unsafe ⇒Elim, lines 7.c,7.d
7.f  false falseIntro, lines 6,7.e
8¬(P-safe∧W-safe)P-safe W-safe  RAA, line 7
9subproof:¬¬(R-safe∧W-safe) ⊢ falseR-safe W-safe ⊢   
9.a  ¬¬(R-safe∧W-safe)R-safe W-safe Premise for subproof
9.b  R-safe∧W-safeR-safe W-safe ¬Elim, line 9.a
9.c  W-safeW-safe ∧Elim, line 9.b
9.d  W-safe⇒¬W-unsafeW-safe W-unsafe WaterWorld axiom
9.e  ¬W-unsafeW-unsafe ⇒Elim, lines 9.c,9.d
9.f  false falseIntro, lines 6,9.e
10¬(R-safe∧W-safe)R-safe W-safe  RAA, line 9
11Q-has-1⇒P-safe∧R-safe∨P-safe∧W-safe∨R-safe∧W-safe Q-has-1 P-safe R-safe P-safe W-safe R-safe W-safe   Theorem: Allowed by problem statement
12P-safe∧R-safe∨P-safe∧W-safe∨R-safe∧W-safe P-safe R-safe P-safe W-safe R-safe W-safe   ⇒Elim, lines 1,11
13R-safe∧W-safe∨P-safe∧R-safe∨P-safe∧W-safe R-safe W-safe P-safe R-safe P-safe W-safe   Theorem: ∨ commutes, line 12
14P-safe∧R-safe∨P-safe∧W-safe P-safe R-safe P-safe W-safe   CaseElim, lines 8,13
15P-safe∧W-safe∨P-safe∧R-safe P-safe W-safe P-safe R-safe   Theorem: ∨ commutes, line 14
16P-safe∧R-safeP-safe R-safe  CaseElim, lines 10,15
17P-safeP-safe  ∧Elim, line 16

Alternatively, the subproofs could easily have been pulled out into lemmas. Just like using subroutines in a program, that would make the proof somewhat clearer, even though in this case each lemma would be used only once.

Observe how the two subproofs have some identical lines (7.c-7.f and 9.c-9.f). It would be incorrect to replace those lines in the second subproof with a citation of the results of the first subproof. First, because the previous subproof had been completed, and moreover, the two subproofs have different premises. This is analogous to two subroutines that happen to have some identical code lines, even through they are called separately and have different parameters.

Note:
Interestingly, we didn't need to use R-safeR-safe as a premise. (In fact, we nearly proved that ¬R-safeR-safe would have been inconsistent with the other premises.)

Exercise 15

Starting from the WaterWorld axiom Q-has-1⇒P-safe∧R-safe∧W-unsafe∨P-safe∧R-unsafe∧W-safe∨P-unsafe∧R-safe∧W-safe Q-has-1 P-safe R-safe W-unsafe P-safe R-unsafe W-safe P-unsafe R-safe W-safe , we could prove the following theorem cited in the previous problem: Q-has-1⇒P-safe∧R-safe∨P-safe∧W-safe∨R-safe∧W-safe Q-has-1 P-safe R-safe P-safe W-safe R-safe W-safe .

Prove the following theorem which is slightly simpler: φ⇒ψ∧θ∨δ∧ε ⊢ φ⇒ψ∨δ φ ψ θ δ ε ⊢ φ ψ δ .

Note:

If you have trouble, first prove an even simpler version: φ⇒ψ∧θ ⊢ φ⇒ψφ ψ θ ⊢ φ ψ.

Exercise 16

[Practice problem——solution provided.]

Show that the ¬Elim inference rule is redundant in our system. In other words, without using ¬Elim, prove that ¬¬φ ⊢ φφ ⊢ φ.

Solution

Table 5
1¬¬φφ  Premise
2subproof:¬φ ⊢ falseφ ⊢   
2.a  ¬φφ Premise for subproof
2.b  false falseIntro, lines 1,2.a
3φφ  RAA, line 2

Exercise 17

Show that the ¬Intro inference rule is redundant in our system. In other words, without using ¬Intro, prove that φ ⊢ ¬¬φφ ⊢ φ. To make sure that you're not hiding any uses of ¬Intro, also do not use any previous theorems.

Exercise 18

Show that the CaseElim inference rule is redundant in our system. For brevity, we'll just consider the left-hand version. In other words, without using CaseElim, prove that φ∨ψ, ¬φ ⊢ ψφ ψ, φ ⊢ ψ. To make sure that you're not hiding any uses of CaseElim, also do not use any previous theorems.

Exercise 19

  • State where on a board pirates could be positioned, so that: P-has-1∧U-has-1∧W-has-1P-has-1 U-has-1 W-has-1, but X-safeX-safe.
  • Compare this with a previous theorem, B-has-1∧G-has-1∧J-has-1⇒K-unsafe B-has-1 G-has-1 J-has-1 K-unsafe , the same idea shifted down a couple of rows. Suppose we try to translate this theorem's proof so as to conclude ¬X-safeX-safe (clearly untrue, by the above). What is the first step of the modified proof which doesn't hold when BB,GG,JJ,KK are mindlessly replaced with PP,UU,WW,XX, respectively? (Just give a line number; no explanation needed. Your answer will be of the form “Lemma A line 1” or “main proof line 2”.)
  • We've just seen that the mindless changing of location-names introduces false steps. But we can be a little smarter, and modify the false step to get a formula which is true, and is also still in the spirit of the original proof. We can thus patch the problem from the previous part, and continue on modifying the original proof for several more steps. But clearly we can't translate the entire original proof; we eventually hit a more fundamental snag: a formula which isn't true, yet can't be patched up, either. What is the first line that can't be patched? (Again, just give a line number; no explanation needed. Your answer will be of the form “Lemma A line 1” or “main proof line 2”.)

Exercise 20

Which is worse, having an unsound (but complete) inference system or an incomplete (but sound) one? Why?

Collection Navigation

Content actions

Download 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