This is a proof generator and checker for the Fitch-style natural deduction system found in forall x: Calgary. You can work through exercises from the textbook or experiment with arguments of your own. If you get stuck, you can request hints to help you complete your proof one step at a time. For the source code and further details, see 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) |