NOTE: the program lets you drop the outermost parentheses on formulas with a binary main connective, e.g. P>(Q&R) rather than (P>(Q&R)). Since the letter 'v' is used for disjunction, it can't be used as a variable.

A description of the rules this program implements can be found in this pdf. See the forallx@syr textbook for more details on the rules. Note that some multi-line rules require lines to be cited in a certain order. For example, in an application of disjunction elimination with citation "∨E j, k-l, m-n", line j must be the disjunction, k must be an assumption of the left disjuct, and m an assumption of the right disjunct. The only multi-line rules that are set up so that order doesn't matter are ∧I, →E, and ¬E.

The rule selection menu in FitchFX has different abbreviations for the rules. For example: >E instead of →E, or &E instead of ∧E. See the "Symbols" reference above for the keyboard substitutes that FitchFX uses for the various logical symbols.

Some (importable) sample proofs in the "plain" notation are here. See this pdf for an example of how Fitch proofs typeset in LaTeX look. To typeset these proofs you will need Johann Klüwer's fitch.sty. (If you don't want to install this file, you can just include it in the the same directory as your tex source file.)