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 or individual constant. Note also that quantifiers are enclosed by parentheses, e.g. (Ex)Rax rather than ExRax, or (Ax)(Fx>Gx) rather than Ax(Fx>Gx).

NOTE: the order in which rule lines are cited is important for multi-line rules. For example, in an application of conditional elimination with citation "j,k →E", line j must be the conditional, and line k must be its antecedent, even if line k actually precedes line j in the proof. The only multi-line rules which are set up so that order doesn't matter are &I and ⊥I.

NOTE: as with the propositional rules, the order in which lines are cited matters for multi-line rules.

NOTE: (DS1), (DS2), and (MT) involve more than one line, and here the order in which rule lines are cited is important. E.g. to use (MT) 'A>B, ~B |- ~A', the line number of the conditional A>B needs to be cited first, and that of the negated consequent ~B second.

Some (importable) sample proofs in the "plain" notation are here.

Note that proofs can also be exported in "pretty print" notation (with unicode logic symbols) or LaTeX. 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.)