Natural Deduction Proof Generator & Checker

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