# The Rules of the Lemmon 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 got to Help with Language. Note that this text is not an introduction to formal logic. It presupposes some acquaintance with a deductive system. If you are completely new to natural deduction, you should try to get hold of a copy of E.J. Lemmon's "Beginning Logic" and read the introductory chapters.

• &E (elimination of a conjunction) allows you to move either to p or to q given that p & q is a line of the proof.
• &I (introduction of a conjunction) allows you to move from p, q as lines to p & q or to q & p.
• ->E (elimination of a conditional) allows you to move from p, p -> q to q. Often this is called 'modus ponens' or 'affirming the antecedent'.
• ~~E (elimination of double negation) allows you to move from ~~p to p.
• vI (introduction of a disjunction) allows you to move from p to p v q or to q v p where q is an arbitrary disjunct. Note that you must specify this disjunct in R1 when you are using the proof-builder. This rule is often called addition.
• vE (elimination of a disjunction) allows you to move from p v q, p -> r, q -> r to r.
• ->I (introduction of a conditional) is used to complete a conditional proof. Recall that to discharge the assumption you need to highlight the assumption and the last line.
• ~I (introduction of a negation, also known as RAA - reductio ad absurdum) is used to complete an indirect proof. The last line must be an explicit contradiction.

Rules not described here are required for predicate logic. They will be treated at a later time.

© Christian Gottschall / christian.gottschall@posteo.de / 2012-03-31 01:19:53