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

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)
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.