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 17, Exercise B — Add the missing justifications to the following proofs: | |
|---|---|
| 1. | P ∧ S, S → R ∴ R ∨ E |
| 2. | A → D ∴ (A ∧ B) → (D ∨ E) |
| 3. | ¬L → (J ∨ L), ¬L ∴ J |
| Chapter 17, Exercise C — Give a proof for each of the following arguments: | |
|---|---|
| 1. | J → ¬J ∴ ¬J |
| 2. | Q → (Q ∧ ¬Q) ∴ ¬Q |
| 3. | A → (B → C) ∴ (A ∧ B) → C |
| 4. | K ∧ L ∴ K ↔ L |
| 5. | (C ∧ D) ∨ E ∴ E ∨ D |
| 6. | A ↔ B, B ↔ C ∴ A ↔ C |
| 7. | ¬F → G, F → H ∴ G ∨ H |
| 8. | (Z ∧ K) ∨ (K ∧ M), K → D ∴ D |
| 9. | P ∧ (Q ∨ R), P → ¬R ∴ Q ∨ E |
| 10. | S ↔ T ∴ S ↔ (T ∨ S) |
| 11. | ¬(P → Q) ∴ ¬Q |
| 12. | ¬(P → Q) ∴ P |
| Chapter 18, Exercise A — Give a proof for each of the following arguments: | |
|---|---|
| 1. | A → B, A → C ∴ A → (B ∧ C) |
| 2. | (A ∧ B) → C ∴ A → (B → C) |
| 3. | A → (B → C) ∴ (A → B) → (A → C) |
| 4. | A ∨ (B ∧ C) ∴ (A ∨ B) ∧ (A ∨ C) |
| 5. | (A ∧ B) ∨ (A ∧ C) ∴ A ∧ (B ∨ C) |
| 6. | A ∨ B, A → C, B → D ∴ C ∨ D |
| 7. | ¬A ∨ ¬B ∴ ¬(A ∧ B) |
| 8. | A ∧ ¬B ∴ ¬(A → B) |
| Chapter 18, Exercise C — Practice proving sentences from no premises: | |
|---|---|
| 1. | ¬A → (A → ⊥) |
| 2. | ¬(A ∧ ¬A) |
| 3. | ((A → C) ∧ (B → C)) → ((A ∨ B) → C) |
| 4. | ¬(A → B) → (A ∧ ¬B) |
| 5. | (¬A ∨ B) → (A → B) |
| Chapter 18, Exercise D — Practice proving arguments requiring IP: | |
|---|---|
| 1. | ∴ ¬¬A → A |
| 2. | ¬A → ¬B ∴ B → A |
| 3. | A → B ∴ ¬A ∨ B |
| 4. | ∴ ¬(A ∧ B) → (¬A ∨ ¬B) |
| 5. | A → (B ∨ C) ∴ (A → B) ∨ (A → C) |
| 6. | ∴ (A → B) ∨ (B → A) |
| 7. | ∴ ((A → B) → A) → A |
| Chapter 19, Exercise A — Add the missing justifications to the following proofs: | |
|---|---|
| 1. | W → ¬B, A ∧ W, B ∨ (J ∧ K) ∴ K |
| 2. | L ↔ ¬O, L ∨ ¬O ∴ L |
| 3. | Z → (C ∧ ¬N), ¬Z → (N ∧ ¬C) ∴ N ∨ C |
| Chapter 19, Exercise B — Give a proof for each of the following arguments: | |
|---|---|
| 1. | E ∨ F, F ∨ G, ¬F ∴ E ∧ G |
| 2. | M ∨ (N → M) ∴ ¬M → ¬N |
| 3. | (M ∨ N) ∧ (O ∨ P), N → P, ¬P ∴ M ∧ O |
| 4. | (X ∧ Y) ∨ (X ∧ Z), ¬(X ∧ D), D ∨ M ∴ M |
| Chapter 20, Exercise A — Show that each of the following sentences is a theorem: | |
|---|---|
| 1. | O → O |
| 2. | N ∨ ¬N |
| 3. | J ↔ (J ∨ (L ∧ ¬L)) |
| 4. | ((A → B) → A) → A |
| Chapter 20, Exercise B — Give a proof for each of the following arguments: | |
|---|---|
| 1. | C → (E ∧ G), ¬C → G ∴ G |
| 2. | M ∧ (¬N → ¬M) ∴ (N ∧ M) ∨ ¬M |
| 3. | (Z ∧ K) ↔ (Y ∧ M), D ∧ (D → M) ∴ Y → Z |
| 4. | (W ∨ X) ∨ (Y ∨ Z), X → Y, ¬Z ∴ W ∨ Y |