80-310/610 Logic and Computation Fall 2001

Solutions to Homework #11

3. The first derivation is used in the second one, at the position marked * (there wasn’t enough room to write it in). a.

\begin{aligned}\begin{matrix}\begin{aligned}[p]_{1} & [p ↔ ¬p]_{3} \\ & ¬p \end{aligned} & [p]_{1} \\ ⊥ \end{matrix} ; 1 ; ¬p & & [p ↔ ¬p]_{3} \\ & p \end{aligned}  \begin{matrix}\begin{aligned}[p]_{2} & [p ↔ ¬p]_{3} \\ & ¬p \end{aligned} & [p]_{2} \\ ⊥ \end{matrix} ; 2 ; ¬p ⊥ 3 ¬(p ↔ ¬p)
b. \begin{aligned}[∃y ∀x (S(y, x) ↔ ¬S(x, x))]_{2} & {[∀x (S(y, x) ↔ ¬S(x, x))]_{1} \atop S(y, y) ↔ ¬S(y, y)} ; * ; ⊥ \\ & 1 \\ ⊥ \end{aligned} ; 2 ; ¬∃y ∀x (S(y, x) ↔ ¬S(x, x))

4. Forwards direction:

[∃x (φ(x) ∧ ψ)]_{2}  \begin{matrix}{[φ(x) ∧ ψ]_{1} \atop φ(x)} ; ∃x φ(x) & {[φ(x) ∧ ψ]_{1} \atop ψ} \\ ∃x φ(x) ∧ ψ \end{matrix} 1 ∃x φ(x) ∧ ψ 2 ∃x (φ(x) ∧ ψ) → ∃x φ(x) ∧ ψ

Backwards direction:

{[∃x φ(x) ∧ ψ]_{2} \atop ∃x φ(x)}  \begin{matrix}[φ(x)]_{1} & {[∃x φ(x) ∧ ψ]_{2} \atop ψ} \\ φ(x) ∧ ψ \end{matrix} ; ∃x (φ(x) ∧ ψ) 1 ∃x (φ(x) ∧ ψ) 2 ∃x φ(x) ∧ ψ → ∃x (φ(x) ∧ ψ)

7. Forwards direction:

\begin{matrix}[¬∃x φ(x)]_{2} & \begin{matrix}[φ(x)]_{1} \\ ∃x φ(x) \end{matrix} \\ ⊥ \end{matrix} ; 1 ; ¬φ(x) ∀x ¬φ(x) 2 ¬∃x φ(x) → ∀x ¬φ(x)

Backwards direction:

[∃x φ(x)]_{2}  \begin{aligned}[φ(x)]_{1} & & {[∀x ¬φ(x)]_{3} \atop ¬φ(x)} \\ & ⊥ \end{aligned} 1 ⊥ 2 ¬∃x φ(x) 3 ∀x ¬φ(x) → ¬∃x φ(x)

9.

\begin{aligned}{∀x L(x, b) \atop L(b, b)} & {∀x (L(b, x) → x = m) \atop L(b, b) → b = m} \\ & b = m \end{aligned}

10. For I_{2}:

\begin{matrix}{∀x, y, z (x = y ∧ z = y → x = z) \atop u = u ∧ v = u → u = v} & \begin{matrix}{∀x (x = x) \atop u = u} & [v = u]_{1} \\ u = u ∧ v = u \end{matrix} \\ u = v \end{matrix} ; 1 ; v = u → u = v ; ∀v, u (v = u → u = v)

In this derivation, I’ve combined instances of the ∀ rules. On the top left, note that I am substituting u, u, and v for x, y, and z respectively.

For I_{3}, use I_{2}:

\begin{matrix}∀x, y, z (x = y ∧ z = y → x = z & \begin{matrix}{[x = y ∧ y = z]_{1} \atop x = y} & {[x = y ∧ y = z]_{1} \atop y = z} ; * ; z = y \\ x = y ∧ z = y \end{matrix} \\ x = z \end{matrix} ; 1 ; x = y ∧ y = z → x = z ; ∀x, y, z (x = y ∧ y = z → x = z)

Here the derivation of I_{2} is used at *.

\begin{aligned}\begin{matrix}[φ]_{1} \\ φ ∨ ¬φ \end{matrix} & [¬(φ ∨ ¬φ)]_{2} \\ & ⊥ \end{aligned} ; 1 ; ¬φ ; φ ∨ ¬φ [¬(φ ∨ ¬φ)]_{2} ⊥ 2 RAA φ ∨ ¬φ