This is a proof generator and checker for the Fitch-style natural deduction system found in forall x: Calgary. It is based on the Open Logic Project proof checker. More information can be found in the ND-Prover repository.
| Chapter 36, Exercise B — Add the missing justifications to the following proofs: | |
|---|---|
| 1. | ∀x ∃y (R(x, y) ∨ R(y, x)), ∀x ¬R(m, x) ∴ ∃x R(x, m) |
| 2. | ∀x (∃y L(x, y) → ∀z L(z, x)), L(a, b) ∴ ∀x L(x, x) |
| 3. | ∀x (J(x) → K(x)), ∃x ∀y L(x, y), ∀x J(x) ∴ ∃x (K(x) ∧ L(x, x)) |
| Chapter 36, Exercise E — Give a proof for each of the following arguments: | |
|---|---|
| 1. | ∴ ∀x F(x) → ∀y (F(y) ∧ F(y)) |
| 2. | ∀x (A(x) → B(x)), ∃x A(x) ∴ ∃x B(x) |
| 3. | ∀x (M(x) ↔ N(x)), M(a) ∧ ∃x R(x, a) ∴ ∃x N(x) |
| 4. | ∀x ∀y G(x, y) ∴ ∃x G(x, x) |
| 5. | ∴ ∀x R(x, x) → ∃x ∃y R(x, y) |
| 6. | ∴ ∀y ∃x (Q(y) → Q(x)) |
| 7. | N(a) → ∀x (M(x) ↔ M(a)), M(a), ¬M(b) ∴ ¬N(a) |
| 8. | ∀x ∀y (G(x, y) → G(y, x)) ∴ ∀x ∀y (G(x, y) ↔ G(y, x)) |
| 9. | ∀x (¬M(x) ∨ L(j, x)), ∀x (B(x) → L(j, x)), ∀x (M(x) ∨ B(x)) ∴ ∀x L(j, x) |
| Chapter 37, Exercise A — Give a proof for each of the following arguments: | |
|---|---|
| 1. | A → ∀x B(x) ∴ ∀x (A → B(x)) |
| 2. | ∃x (A → B(x)) ∴ A → ∃x B(x) |
| 3. | ∴ ∀x (A(x) ∧ B(x)) ↔ (∀x A(x) ∧ ∀x B(x)) |
| 4. | ∴ ∃x (A(x) ∨ B(x)) ↔ (∃x A(x) ∨ ∃x B(x)) |
| 5. | A ∨ ∀x B(x) ∴ ∀x (A ∨ B(x)) |
| 6. | ∀x (A(x) → B) ∴ ∃x A(x) → B |
| 7. | ∃x (A(x) → B) ∴ ∀x A(x) → B |
| 8. | ∴ ∀x (A(x) → ∃y A(y)) |
| Chapter 37, Exercise B — Give a proof for each of the following arguments: | |
|---|---|
| 1. | ∀x R(x, x) ∴ ∀x ∃y R(x, y) |
| 2. | ∀x ∀y ∀z ((R(x, y) ∧ R(y, z)) → R(x, z)) ∴ ∀x ∀y (R(x, y) → ∀z (R(y, z) → R(x, z))) |
| 3. | ∀x ∀y ∀z ((R(x, y) ∧ R(y, z)) → R(x, z)), ∀x ∀y (R(x, y) → R(y, x)) ∴ ∀x ∀y ∀z ((R(x, y) ∧ R(x, z)) → R(y, z)) |
| 4. | ∀x ∀y (R(x, y) → R(y, x)) ∴ ∀x ∀y ∀z ((R(x, y) ∧ R(x, z)) → ∃u (R(y, u) ∧ R(z, u))) |
| 5. | ∴ ¬∃x ∀y (A(x, y) ↔ ¬A(y, y)) |
| Chapter 37, Exercise C — Practice proving arguments requiring IP: | |
|---|---|
| 1. | ∀x A(x) → B ∴ ∃x (A(x) → B) |
| 2. | A → ∃x B(x) ∴ ∃x (A → B(x)) |
| 3. | ∀x (A ∨ B(x)) ∴ A ∨ ∀x B(x) |
| 4. | ∴ ∃x (A(x) → ∀y A(y)) |
| 5. | ∴ ∃x (∃y A(y) → A(x)) |
| Chapter 39, Exercise A — Practice proving arguments involving identity: | |
|---|---|
| 1. | P(a) ∨ Q(b), Q(b) → b = c, ¬P(a) ∴ Q(c) |
| 2. | m = n ∨ n = o, A(n) ∴ A(m) ∨ A(o) |
| 3. | ∀x x = m, R(m, a) ∴ ∃x R(x, x) |
| 4. | ∀x ∀y (R(x, y) → x = y) ∴ R(a, b) → R(b, a) |
| 5. | ¬∃x ¬x = m ∴ ∀x ∀y (P(x) → P(y)) |
| 6. | ∃x J(x), ∃x ¬J(x) ∴ ∃x ∃y ¬x = y |
| 7. | ∀x (x = n ↔ M(x)), ∀x (O(x) ∨ ¬M(x)) ∴ O(n) |
| 8. | ∃x D(x), ∀x (x = p ↔ D(x)) ∴ D(p) |
| 9. | ∃x ((K(x) ∧ ∀y (K(y) → x = y)) ∧ B(x)), K(d) ∴ B(d) |
| 10. | ∴ P(a) → ∀x (P(x) ∨ ¬x = a) |