The Rules of the Fitch System

(this text by Steven DeHaven, Calgary, and Christian Gottschall, Vienna)

This help is simply a brief summary of the rules. If you need help with the use of the applet go to Help with Applet. If you need help with the formal language go to Help with Language. The sole purpose of this help is to explain the "mechanics" of the use of the builder. The outermost pair of parentheses, if there is such, are standardly omitted.

Reit allows you to reiterate an accessible line.
&E allows you to move either to p or to q given that p & q as an accessible line. Note that when you are working within assumptions you typically will need to reiterate an accessible line if you wish to appeal to it within the scope of the assumption.
&I allows you to move from p, q as lines to p & q or to q & p.
->E allows you to move from p, p -> q to q. Often this is called 'modus ponens' or 'affirming the antecedent'.
MT allows you to move from p -> q , ~q to ~p. This, the rule we call 'modus tollens'. You may also know it as 'denying the consequent'.
DS allows you to move from p v q, ~p to q or from p v q, ~q to p. This rule we call 'disjunctive syllogism'.
~~E allows you to move from ~~p to p.
~~I allows you to move from p to ~~p.
vI allows you to move from p to p v q or to q v p. Note that you must specify the disjunct in R1 when you are using the proof-builder. This is often called addition.
vE allows you to move from p v q, p -> r, q -> r to r.
<->E allows you to move from p <-> q to either (p -> q) & (q -> p) or (q -> p) & (p -> q).
<->I allows you to move from (p -> q) & (q -> p) to p <-> q or to q <-> p.
->I is used to complete a conditional proof. Recall that to discharge the assumption you need to highlight the assumption and the last line.
~I is used to complete an indirect proof. The last line must be an explicit contradiction.
~E can also be used to complete an indirect proof. Again the last line must be an explicit contradiction. And it can only be applied where the assumption is a negation ~p.