Skip to content Skip to navigation

Connexions

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

Navigation

Content Actions
  • Download module PDF
  • Add to ...
    Add the module to:
    • My Favorites
    • A lens
    • An external social bookmarking service
    • My Favorites (What is '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 (What is 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.

    • External bookmarks
  • E-mail the authors

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

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 domain axiom,
  • 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, (χ∨υ) ⊢ (υ∨χ)(χ∨υ) ⊢ (υ∨χ).

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 (φ∧ψ), (φ→θ), (ψ→δ) ⊢ (θ∧δ)(φ∧ψ), (φ→θ), (ψ→δ) ⊢ (θ∧δ).

hint:

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): ¬(φ∨ψ) ⊢ ¬φ¬(φ∨ψ) ⊢ ¬φ.

hint:

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 4

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

hint:

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 have nothing corresponding to DeMorgan's Law. Prove each of the following versions.

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

Exercise 8

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 9

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

  1. (φ→ψ) ⊢ (¬φ∨ψ)(φ→ψ) ⊢ (¬φ∨ψ)
  2. (¬φ∨ψ) ⊢ (φ→ψ)(¬φ∨ψ) ⊢ (φ→ψ)

Exercise 10

Prove the following: (φ→ψ), (ψ→φ) ⊢ ((φ∧ψ)∨(¬φ∧¬ψ))(φ→ψ), (ψ→φ) ⊢ ((φ∧ψ)∨(¬φ∧¬ψ))

Exercise 11

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.

    hint:

    Use RAA two or three times.

Exercise 12

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

1X-has-1X-has-1  ____________
2____________  WaterWorld domain 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-unsafe)(W-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-safe)(W-unsafe∧Y-safe) CaseElim (left), lines ____________, where (φ=____________)(φ ____________), and (ψ=____________)(ψ ____________)
5.c  ____________ ____________
5.d  (W-unsafe∨Y-unsafe)(W-unsafe∨Y-unsafe) ____________
6((W-safe∧Y-unsafe)∨¬(W-safe∧Y-unsafe))((W-safe∧Y-unsafe)∨¬(W-safe∧Y-unsafe))  Theorem: Excluded Middle, where (χ=____________)(χ ____________)
7(W-unsafe∨Y-unsafe)(W-unsafe∨Y-unsafe)  ____________

Exercise 13

[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 domain 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-unsafe¬Y-unsafe.

Solution 13

1Q-has-1Q-has-1  Premise
2X-has-1X-has-1  Premise
3¬Y-unsafe¬Y-unsafe  Premise
4(W-unsafe∨Y-unsafe)(W-unsafe∨Y-unsafe)  Theorem: above problem, line 2
5(Y-unsafe∨W-unsafe)(Y-unsafe∨W-unsafe)  Theorem: ∨∨ commutes, line 4
6W-unsafeW-unsafe  CaseElim, lines 3,5
7subproof:¬¬(P-safe∧W-safe) ⊢ false¬¬(P-safe∧W-safe) ⊢   
7.a  ¬¬(P-safe∧W-safe)¬¬(P-safe∧W-safe) Premise for subproof
7.b  (P-safe∧W-safe)(P-safe∧W-safe) ¬¬Elim, line 7.a
7.c  W-safeW-safe ∧∧Elim, line 7.b
7.d  (W-safe→¬W-unsafe)(W-safe→¬W-unsafe) WaterWorld domain axiom
7.e  ¬W-unsafe¬W-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) ⊢ false¬¬(R-safe∧W-safe) ⊢   
9.a  ¬¬(R-safe∧W-safe)¬¬(R-safe∧W-safe) Premise for subproof
9.b  (R-safe∧W-safe)(R-safe∧W-safe) ¬¬Elim, line 9.a
9.c  W-safeW-safe ∧∧Elim, line 9.b
9.d  (W-safe→¬W-unsafe)(W-safe→¬W-unsafe) WaterWorld domain axiom
9.e  ¬W-unsafe¬W-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
11(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)))  Theorem: Allowed by problem statement
12(((P-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
13((R-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
14((P-safe∧R-safe)∨(P-safe∧W-safe))((P-safe∧R-safe)∨(P-safe∧W-safe))  CaseElim, lines 8,13
15((P-safe∧W-safe)∨(P-safe∧R-safe))((P-safe∧W-safe)∨(P-safe∧R-safe))  Theorem: ∨∨ commutes, line 14
16(P-safe∧R-safe)(P-safe∧R-safe)  CaseElim, lines 10,15
17P-safeP-safe  ∧∧Elim, line 16 — Whew!

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-safe¬R-safe would have been inconsistent with the other premises.)

Exercise 14

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: (φ→((ψ∧θ)∨(δ∧κ))) ⊢ (φ→(ψ∨δ))(φ→((ψ∧θ)∨(δ∧κ))) ⊢ (φ→(ψ∨δ)).

hint:

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

Exercise 15

[Practice problem—solution provided.]

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

Solution 15

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

Exercise 16

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

Exercise 17

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 (φ∨ψ), ¬φ ⊢ ψ(φ∨ψ), ¬φ