PHI 12 Proof Rules

Conjunction introduction

1. A

2. B

3. A /\ B :/\I 1,2

Conjunction elimination (option 1)

1. A /\ B

2. A :/\E1

can only apply to sentences where conjunction is main logical operator

Conjunction elimination (option 2)

1. A /\ B

2. B :/\E1

can only apply to sentences where conjunction is main logical operator

Conditional elimination

1. A -> B

2. A

3. B :->E 1,2

also called modus ponens, always cite conditional first, followed by the antecedents

Conditional introduction

1. A :AS

2. B

3. A -> B :->I 1-2

To cite an individual line when applying a rule

1. the line must come before the line where the rule is applied, but

2. not occur within a subproof that has been closed before the line where the rule is applied

discharging

closing a subproof

to cite a subproof when applying a rule

1. the cited subproof must come entirely before the application of the rule where it is cited,

2. the cited subproof must not lie within some other closed subproof which is closed at the line it is cited, and

3. its last line of the cited subproof must not occur inside a nested subproof

soundness

if A entails B syntactically, then A entails B semantically

completeness

if A entails B semantically, then A entails B syntactically

Biconditional introduction

1. A :AS

2. B

3. B :AS

4. A

5. A <-> B :<->I 1-2, 3-4

Biconditional elimination (option 1)

1. A <-> B

2. A

3. B :<->E 1, 2

Biconditional elimination (option 2)

1. A <-> B

2. B

3. A :<->E 1-2

Disjunction introduction (option 1)

1. A

2. A \/ B :\/I 1

Disjunction introduction (option 2)

1. A

2. B \/ A :\/I 1

Disjunction elimination

1. A \/ B

2. A :AS

3. C

4. B :AS

5. C

6. C :\/E 1, 2-3, 4-5

also called proof by cases

Negation elimination

1. ¬A

2. A

3. _|_ :¬E1,2

new special atomic sentence of TFL, but one which can only ever have the truth value False

Negation introduction

1. A :AS

2. _|_

3. ¬A :¬I1-2

The Law of Non-Contradiction

1. A /\ ¬A :AS

2. ¬A :/\E1

3. A :/\E1

4. _|_ :¬E2,3

5. ¬(A /\ ¬A) :¬I1-4

Indirect proof

1. ¬A

2. _|_

3. A :IP

allows us to prove A indirectly by assuming its negation

explosion: ex falso quodlibet

from falsehood, anything follows

explosion: ex contradictione quodlibet

from a contradiction, anything follows

explosion

1. _|_

2. A :X1

reiteration

1. A

2. A :R1