Basic Connectives
Negation (¬)
Rules
Double-Negation Introduction: Given A, we can infer ¬¬A.
Double-Negation Elimination: Given ¬¬A, we can infer A.
Truth Table
<tr><th>A</th><th>¬A</th></tr>
<tr><td>0</td><td>1</td></tr>
<tr><td>1</td><td>0</td></tr>
Conjuction (∧)
Rules
Conjunction Introduction: Given A and given B, we can infer A∧B.
Conjunction Elimination: Given A∧B, we can infer A. Given A∧B, we can infer B.
Truth Table
<tr><th>A</th><th>B</th><th>A∧B</th></tr>
<tr><td>0</td><td>0</td><td>0</td></tr>
<tr><td>0</td><td>1</td><td>0</td></tr>
<tr><td>1</td><td>0</td><td>0</td></tr>
<tr><td>1</td><td>1</td><td>1</td></tr>
Disjunction (∨)
Rules
Disjunction Introduction: Given A, we can infer A∨B. Given B, we can infer A∨B.
Disjunction Elimination: Given A∨B, and given C assuming A, and given C assuming B, we can infer C and discharge the assumptions A and B.
Truth Table
<tr><th>A</th><th>B</th><th>A∨B</th></tr>
<tr><td>0</td><td>0</td><td>0</td></tr>
<tr><td>0</td><td>1</td><td>1</td></tr>
<tr><td>1</td><td>0</td><td>1</td></tr>
<tr><td>1</td><td>1</td><td>1</td></tr>
Conditional (→)
Rules
Conditional Introduction (Conditional Proof): Given B assuming A, we can infer A→B and discharge the assumption A.
Conditional Elimination (Modus Ponens): Given A and given A→B, we can infer B.
Denying the Consequent (Modus Tollens): Given A→B and ¬B, we can infer ¬A.
Truth Table
<tr><th>A</th><th>B</th><th>A→B</th></tr>
<tr><td>0</td><td>0</td><td>1</td></tr>
<tr><td>0</td><td>1</td><td>1</td></tr>
<tr><td>1</td><td>0</td><td>0</td></tr>
<tr><td>1</td><td>1</td><td>1</td></tr>
Biconditional (↔)
Rules
Biconditional Introduction: Given A→B and given B→A, we can infer A↔B.
Biconditional Elimination: Given A↔B, we can infer (A→B)∧(B→A)
Truth Table
<tr><th>A</th><th>B</th><th>A↔B</th></tr>
<tr><td>0</td><td>0</td><td>1</td></tr>
<tr><td>0</td><td>1</td><td>0</td></tr>
<tr><td>1</td><td>0</td><td>0</td></tr>
<tr><td>1</td><td>1</td><td>1</td></tr>
Other inference rules
Reducto ad absurdum
Given A assuming B, and given ¬A assuming B, we can infer ¬B and discharge the assumption B.