COM2107 Logic Rules

→ E / Modus Ponens / Implication Elimination

If you have a conditional statement and its antecedent, you can derive the consequent.

1. A → B

2. A

3. B (→ E 1, 2)

→ I / Implication Introduction

To prove A→B, you assume A is true.

If you can use that assumption to prove B, you can conclude A→B (and discharge the assumption)

∧I / Conjunction Introduction

If you have two separate statements, you can join them together with an "and"

1. A

2. B

3. A ^ B (^I 1, 2)

^E / Conjunction Elimination

If you have a conjunction, you can strip away either side of it.

1. A^B

2. A (^E, 1)

3. B (^E, 2)

vI / Disjunction Introduction

If you have a true statement, you can add literally any other statement to it with an "or"

1. A

2. A v B (vI 1)

vE / Disjunction Elimination

If you know A∨B is true, and you can show that A leads to C, and B also leads to C, then C must be true.

Basically, need to open sub boxes, assume one side is True (ie Assume A then work out C) and vice versa. Can only use that assumed value

From A∨B, a subproof [A]…C, and a subproof [B]…C, you can infer C

¬I / Negation Introduction

If assuming A leads to a contradiction (⊥), then A must be false

Assume [A] … derive ⊥ ⟹ conclude ¬A#

¬E / Negation Elimination

If you have both a statement and its negation, you have a contradiction

From A and ¬A, you can infer ⊥

¬¬E / Double Negation Elimination

Double negative cancels out

¬¬A = A

⊥E / Explosion Principle

From a contradiction, absolutely anything follows

1. ⊥

2. B

¬(A∧B) ⟺ ?

¬A∨¬B

¬(A∨B) ⟺ ?

¬A∧¬B

PBC / Reductio ad Absurdum

Temporarily assume the exact opposite of a statement is true

If that assumption leads you to a logical contradiction, you have proven that your assumption was impossible, meaning the original statement must be true.

LEM

I don't know whether A is true or false, but I know it has to be one of them. Let me show you that either way, I can get the value/statement I need.

• Choose your weapon: Look at your proof and figure out what statement (A) would be incredibly useful if it were true.

• Invoke LEM: Write down A∨¬A on a new line.

• Open Cases: Immediately open a subproof assuming A, and then a second subproof assuming ¬A.

• Close the trap: Use ∨E to bring your final conclusion out of the subproofs.