 If Γ or Δ are empty then they are respectively valid or unsatisfiable. An axiom of LK is a sequent Γ → Δ where Γ ∩ Δ ≠ ∅. Thus, the requirement that the same formula occurs at each side of the → sign means that the axioms of LK are valid, for no interpretation can then make all the formulas in Γ true and, simultaneously, make all those in Δ false. LK has two rules per logical connective, plus one extra rule: the cut rule. 