This is a proof checker for the Fitch-style natural deduction system found in *forall x: An Introduction to Formal Logic*. It is a slightly modified version of *this proof checker*. I have modified the names for the rules in the original text of *forall x*, and have therefore updated the code for the proof checker to match.

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

Conclusion:

- Sample Sentence Logic exercises (Chap. 15, ex. C; Chap. 17, ex. B)
- Sample Predicate Logic exercises (Chap. 32, ex. E; Chap. 34, ex. A)

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

PL atomic sentences: (single uppercase letters other than A or E followed bylowercase letters a–w without parentheses) | Pa, Fcdc, 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 SL only: =) |

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

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

For the existential quantifier (PL 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.