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.