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>&not;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&and;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&or;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&rarr;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&harr;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.