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 43, Exercise A — Provide proofs for the following in system K: | |
|---|---|
| 1. | ☐(A ∧ B) ∴ ☐A ∧ ☐B |
| 2. | ☐A ∧ ☐B ∴ ☐(A ∧ B) |
| 3. | ☐A ∨ ☐B ∴ ☐(A ∨ B) |
| 4. | ☐(A ↔ B) ∴ ☐A ↔ ☐B |
| Chapter 43, Exercise B — Provide proofs for the following in system K: | |
|---|---|
| 1. | ¬☐A ∴ ◇¬A |
| 2. | ◇¬A ∴ ¬☐A |
| 3. | ¬◇A ∴ ☐¬A |
| 4. | ☐¬A ∴ ¬◇A |
| Chapter 43, Exercise C — Provide proofs for the following in system K: | |
|---|---|
| 1. | ☐(A → B), ◇A ∴ ◇B |
| 2. | ☐A ∴ ¬◇¬A |
| 3. | ¬◇¬A ∴ ☐A |
| Chapter 43, Exercise D — Provide proofs for the following in system T: | |
|---|---|
| 1. | P ∴ ◇P |
| 2. | ∴ (A ∧ B) ∨ (¬☐A ∨ ¬☐B) |
| Chapter 43, Exercise E — Provide proofs for the following in system S4: | |
|---|---|
| 1. | ☐(☐A → B), ☐(☐B → C), ☐A ∴ ☐☐C |
| 2. | ☐A ∴ ☐(☐A ∨ B) |
| 3. | ◇◇A ∴ ◇A |
| Chapter 43, Exercise F — Provide proofs for the following in system S5: | |
|---|---|
| 1. | ¬☐¬A, ◇B ∴ ☐(◇A ∧ ◇B) |
| 2. | A ∴ ☐◇A |
| 3. | ◇◇A ∴ ◇A |