rules are sound: they preserve counterexamples that lurk in the initial gap	⇒		system is sound: if all gaps close, entailment holds
rules are safe: they do not introduce new counterexamples	⎫ ⎪ ⎪ ⎬ ⎪ ⎪ ⎭	⇒	system is complete: if entailment holds, all gaps close
system is sufficient: any dead-end gap has some lurking counter-example
system is decisive: eventually either all gaps close or there is a dead-end open gap