A very brief introduction to the proof system of the LOGIC PRIMER
Use these links to jump directly to the following topics
--Line of Proof
--Primitive Rules (with links to animations)
--Derived Rules (with links to animations)

Line of Proof

 Each line of proof has four elements, e.g.: 
1,2  (5)  PvQ   4vI
aset lnum sent  ann
aset: The assumption set tracks the dependency of each line on assumptions.
lnum: Line numbers must be sequential and surrounded by parentheses.
sent: A sentence is a well-formed formula of sentential or predicate logic. The accepted connectives and logical operators are: 
~   (not)
&   (and)
v   (or)
->  (if...then...)
<-> (if and only if)
@   (all)
$   (some)
ann: Each rule application must annotated as specified in the text book and shown below.

Rule Annotations

Primitive Rules of Proof

 These are examples of correct annotations; substitute correct numbers in your proofs! Click on links for more information about the specific rule.
There are 10 primitive rules of proof for the sentential system
Assumption
A
Wedge-Elimination
1,2 vE
Wedge-Introduction
1 vI
Ampersand-Elimination
1 &E
Ampersand-Introduction
1,2 &I
Arrow-Elimination
1,2 ->E
Arrow Introduction
1 ->I (2)
Reductio ad Absurdum
1,2 RAA (3)
Double-Arrow Elimination
1 <->E
Double-Arrow Introduction
1,2 <->I
There are six primitive rules of proof for the predicate system
Universal Elimination
1 @E
Universal Introduction
1 @I
Existential Elimination
1,3 $E (2)
 Existential Introduction
1 $I
Identity Elimination
1,2 =E
Identity Introduction
=I

Derived Rules of Proof

 The following derived rules are recognized by the program (see chapter one of the textbook for details):
DN
MTT
v->
DM
HS
FA
TC
 IA
Neg->
vAssoc
&Assoc
vComm
&Trans
Dist
Imp/Exp
 BP
BT
Neg<->
Bitrans
SimDil
SpecDil
ComDil

The rule QE introduced in chapter 3 is also accepted by the program.