Rules of the Formal System

Only write lines that are allowed by these rules. If a move is not specifically allowed by these rules, don’t do it.

Premise (Indicated by “P”) - If "P" is a premise of the argument being derived, then "P" may be written as a new line in the derivation.

Box and Cancel (“DP”)  If the formula indicated by "show" is available below that show line, and there is no other uncancelled "show" between that show line and that formula, then that "show" may be cancelled, and a box may be drawn around that formula and any other lines there may be between it and it's show line. If the relevant show line is line #1, then the derivation is finished.

Conjunction (“CJ”)  If "P" and "Q" are both available lines, they can be joined together by putting a " ^ " between them to make a new sentence "P ^ Q" which may be written as a new line in the derivation.

Simplification (“S”) If "P ^ Q" is an available line, then either "P" or "Q" may be written as a new line in the derivation.

Assumption for Indirect Proof (“AIP”) Whenever you write a show line for any formula, you can write the exact negation of that formula, provided that it is the very next thing you write.

Indirect Proof (“IP”) If any formula and its negation are both available without an uncancelled "show" between them, then the closest "show" that is above them both may be cancelled, and a box may be drawn around the closest one and any other lines there may be between it and that show line. If the relevant show line is line #1, then the derivation is successfully finished. (“Put IP by the "show”)

Double Negation ( "NN”)   You can add two negations to any available formula "Q" to make "~ ~Q," when any available formula begins with two negations that modify the whole rest of that formula, "~ ~P," you can remove those two negations to make "P" and 

Addition (“AD”)   If "P" is an available line, any formula "Q" (“available or not”) can be added to P by putting a wedge "v" between them to make a new sentence "P v Q" or "Q v P" which may be written as a new line in the derivation.

Disjunctive Syllogism (“DS”)  If "P v Q" and "~Q" are both available lines, then "P" may be written as a new line.
If "P v Q" and "~P" are both available lines, then "Q" may be written as a new line.

Commutativity (“CM”) If "P ^ Q" is an available line, then "Q ^ P" may be written as a new line.
If "P v Q" is an available line, then "Q v P" may be written as a new line.

Modus Ponens (“MP”) If "P É Q" and "P" are both available lines, then "Q" may be written as a new line in the derivation.

Modus Tollens (“MT”) If "P É Q" and "~Q" are both available lines, then "~P" may be written as a new line in the derivation.

Assumption for Conditional Proof (“CP”). IF, and ONLY IF, you first write a show line of "Show P É Q" you may write "P" as the very next line, justifying it by "ACP" 

Conditional Proof (“CP”)  IF, and ONLY IF, you subsequently produce "Q" as an available line, and there is no other uncancelled "show" between that show line and that "Q", then that "show" may be cancelled, and a box may be drawn around that formula and any other lines there may be between it and it's show line. If the relevant show line is line #1, then the derivation is successfully finished.  

Rule 13. Repetition (“R”) If "P" appears as an available line, then "P" may be written as a new line.

Rule 14. Pack Biconditional (“PB”) If Q É P and P É Q are both available, then P  Q may be written as a new line in the derivation.

Rule 15. Unpack Biconditional (“UB”) If P  Q is an available line, then Q É P or P É Q may be written as a new line in the derivation.

Rule 16: Theorem (“Thm <number of theorem>“) If T is a theorem containing sentence letters such as "P," "Q," "R" etc, an "instance" of that theorem may be written in as a new line in which every "P" is replaced by exactly the same sentence, and so on. 

De Morgan's Laws (“DML”) Comes in four little rules. 
1. If "~(“R ^ S”)" is an available line, then "~R v ~S" may be written as a new line in the derivation, and 
2. If "~(“R v S”)" is an available line, then "~R ^ ~S" may be written as a new line in the derivation, and 
3. If "~R v ~S" is an available line, then "~(“R ^ S”)" may be written as a new line in the derivation, and 
4. If "~R ^ ~S" is an available line, then "~(“R v S”)" may be written as a new line in the derivation.

Change Quantifier (“CQ”) Comes in eight little rules. 
1. If "xP" is an available line, then "~x~P" may be written as a new line in the derivation, and 
2. If "~xP" is an available line, then "x~P" may be written as a new line in the derivation, and 
3. If "x~P" is an available line, then "~xP" may be written as a new line in the derivation, and 
4. If "~x~P" is an available line, then "xP" may be written as a new line in the derivation, and 
5. If "xP" is an available line, then "~x~P" may be written as a new line in the derivation, and 
6. If "~xP" is an available line, then "x~P" may be written as a new line in the derivation, and 
7. If "x~P" is an available line, then "~xP" may be written as a new line in the derivation, and 
8. If "xP" is an available line, then "~x~P" may be written as a new line in the derivation. 

Universal Instanciation
If "xP" is an available line, then any letter (“name or variable”) can be substituted for all instances of x in P, if every instance of x in P is replaced by the same letter.

Existential Generalization
If P is a line in a derivation and P contains any name or free variable (“not bound by  or “), then a variable bound by  may be substituted for one or more instances of that name or free variable to make xP.