 Although the application of the LK rules affect logic formulas, the rules are seen as manipulating not logic formulas themselves but sequents. Sequents are expressions of the form Γ → Δ, where both Γ and Δ are (possibly empty) sets of formulas. Γ is the sequent’s antecedent and Δ its succedent. Sequents can be interpreted thus: Let I be an interpretation. Then,