φ is T
φ is F
ψ
ψ
ψ ∨ φ
ψ
ψ ← φ
extend possibilities left open by ψ to include those where φ is
T
limit possibilities ruled out by ψ to those where φ is
T