This is a demo of a proof checker for Fitch-style natural
deduction systems found in many popular introductory logic
textbooks. The specific system used here is the one found in
*forall x:
Calgary*. (Although based on *forall x: an Introduction
to Formal Logic*, the proof system in that original
version differs from the one used here and in *forall x:
Calgary*. However, the system also supports the rules used in
the *forall
x: Cambridge* remix.)

Premises (separate with “,” or “;”):

Conclusion:

- Sample Truth-Functional Logic exercises (Chap. 15, ex. C; Chap. 17, ex. B)
- Sample First-Order Logic exercises (Chap. 32, ex. E; Chap. 34, ex. A)

TFL atomic sentences: (single uppercase letters) | A, B, X, etc. |

FOL atomic sentences: (single uppercase letters other than A or E followed bylowercase letters a–w without parentheses, or identities) | Pa, Fcdc, a = d, etc. |

For negation you may use any of the symbols: | ¬ ~ ∼ - − |

For conjunction you may use any of the symbols: | ∧ ^ & . · * |

For disjunction you may use any of the symbols: | ∨ v |

For the biconditional you may use any of the symbols: | ↔ ≡ <-> <> (or in TFL only: =) |

For the conditional you may use any of the symbols: | → ⇒ ⊃ -> > |

For the universal quantifier (FOL only), you may use any of the symbols: | ∀x (∀x) Ax (Ax) (x) ⋀x |

For the existential quantifier (FOL only), you may use any of the symbols: | ∃x (∃x) Ex (Ex) ⋁x |

For a contradiction you may use any of the symbols: | ⊥ XX # |

The following buttons do the following things:

× | = delete this line |

= add a line below this one | |

= add a new subproof below this line | |

= add a new line below this subproof to the parent subproof | |

= add a new subproof below this subproof to the parent subproof |

Apart from premises and assumptions, each line has a cell immediately to its right for entering the justifcation. Click on it to enter the justification as, e.g. “&I 1,2”.

Hopefully it is otherwise more or less obvious how to use it.