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
- Reit allows you to reiterate an accessible
- &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
- 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
- ~~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
- 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
© Christian Gottschall / firstname.lastname@example.org / 2012-03-31 01:19:53