Open Stanford's Fitch Editor •  Open Mike's Classroom • Logic Lesson Plans

Truth Tables, and Logical Equivalences

negation

not

p ¬p
T F
F T

conjunction

and

p q q∧p
T T T
T F F
F T F
F F F

disjunction

or

p q q∨p
T T T
T F T
F T T
F F F

implication

if

p q p⇒q
T T T
T F F
F T T
F F T

bidirectional

if and only if

p q q⇔p
T T T
T F F
F T F
F F T

Fitch Rules of Inference

(AI)

And Introduction

φ1
φ2
...
φn
φ1 ∧ φ2 ∧ ... ∧ φn

(AE)

And Elimination

φ1 ∧ φ2 ∧ ... ∧ φn
φ1
φ2
...
φn

(OI)

Or Introduction

φi
φ1 ∨ φ2 ∨ ... ∨ φn

(OE)

Or Elimination

φ1 ∨ φ2 ∨ ... ∨ φn
φ1 ⇒ ψ
φ2 ⇒ ψ
...
φn ⇒ ψ
ψ

(NI)

Negation Introduction

φ ⇒ ψ
φ ⇒ ¬ ψ
¬ φ

(NE)

Negation Elimination

¬¬φ
φ

(BI)

Biconditional Introduction

φ ⇒ ψ
ψ ⇒ φ
ψ ⇔ φ

(BE)

Biconditional Elimination

ψ ⇔ φ
φ ⇒ ψ
ψ ⇒ φ

(II)

Implication Introduction

φ ⊢ ψ
φ ⇒ ψ

(IE)

Implication Elimination

φ ⇒ ψ
φ
ψ

(UI)

Universal Introduction

φ
∀ν.φ

where ν does not appear free in
both φ and an active assumption

(UE)

Universal Elimintation

∀ν.φ[ν]
φ[τ]

where τ is substitutable for ν in φ

(UE)

Existential Introduction

φ[τ]
∃ν.φ[ν]

where τ does not contain any
universal quantified variables

(EE)

Existential Elimination
(closed sentences)

∃ν.φ[ν]
φ[[τ]]

where τ is not an existing
object constant

(EE)

Existential Elimination
(free variables)

∃ν.φ[ν1, ... , νn]
φ[[π(ν1, ... , νn)]]

where π is not an existing constant

(DC)

Domain Closure

φ[σ1]
...
φ[σn]
∀ν.φ[ν]

(LI)

Linear Induction

φ[a]
∀μ.(φ[μ]→φ[s(μ)]
∀ν.φ[ν];

(TI)

Tree Induction

φ[a]
∀μ.(φ[μ]→φ[f(μ)])
∀μ.(φ[μ]→φ[g(μ)])
∀ν.φ[ν];

(SI)

Structural Induction

φ[a]
φ[b]
∀λ.∀μ.((φ[λ]∧φ[μ])→φ[c(λ, μ)])
∀ν.φ[ν];

Reasoning Tips for Fitch Rules of Inference

  1. If the goal is to prove φ⇒ ψ, then it is a good idea to assume φand see if you can prove ψusing rules of inference. This means you need to start a sub-proof with φ as the assumption.
  2. If the goal is to prove (φ∨ψ), then you only need to prove one of the sentences (choose the one easiest to prove) and use Or Introduction to create the or statement.
  3. If the goal is to prove (φ∧ψ) first prove φ then prove ψ then use And Introduction to provethe conjunction.
  4. If the goal is to prove ¬φ, then you should assume φ is true and then try to prove a contradictionand then use Negation Introduction to prove ¬φ.
  5. If the goal is to prove φ, then you should assume ¬φthen try to prove a contradiction and then use Negation Introduction to prove ¬¬φ and then Negation Elimination to prove φ.
  6. If the goal is to prove ψand thepremises include an implication φ⇒ψ, then you should try to prove φand then use Implication Elimination to prove ψ.
  7. If the goal is to prove χ and the premises include φ∨ψ, then you should try to prove φ⇒χ and then prove ψ⇒χ and then use Or Elimination to prove χ.

Quick Reference for Sub-Proofs

A User's Guide to Implication Introduction

  1. The purpose for using a sub-proof is to introduce an implication statement to the main proof. A logical sentence in the form: φ⇒ψ.
  2. Always open a sub-proof with an assumption.
  3. The assumption should be the antecedent (left side) of the implication you are trying to prove or introduce.This means φ from (1).
  4. Youare free to assume any logical sentence, but it must be the antecedent (left side) to your implication.This means φ from (1).
  5. You cannot use the assumption from the sub-proof in the main proof.
  6. You cannot use any of the conclusions fromthe sub-proofin the main proof.
  7. The reason for (4) and (5) is because their truth value dependson the assumption you made to start the sub-proof, which may or may not be true!
  8. Apply rules of inference to the assumption in a sequence of reasoning steps until you prove the consequent (right side) of the implicationyou are trying to prove. This means you are trying to prove ψ in the sentencefrom (1).
  9. You may use any of the premises or any conclusions from the main proof or the sub-proof within the sub-proof.
  10. Always exit the sub-proof by introducing the implication to the main proof with your assumption as the antecedent (left sideor φ) and your final line of the sub-proof as the consequent (right sideor ψ) of the implication.

Example Proofs

prove r
1. q & p premise
2. q ∨ s ⇒ w premise
3. r ⇔ w ∨ v premise
4. q And Elimination (1)
5. w ∨ v ⇒ r Biconditional Elimination (3)
6. q ∨ s Or Introduction (4)
7. w Implication Elimination (2, 6)
8. w ∨ v Or Introduction (7)
9. r Implication Elimination (5, 8)
prove: ∃x.¬c(x) ⊨ ∀x.c(x)
1. ∃x.¬c(x) premise
2. ¬c([e]) EE(1)
3. ∀x.c(x) Assumption
4. c([e]) UE(3)
5. ∀x.c(x)→c([e]) II(3, 4)
6. ∀x.c(x) Assumption
7. ¬c([e]) Reiteration (2)
8. ∀x.c(x)→¬c([e]) II(6, 7)
9. ¬∀x.c(x) NI(5, 8)