LK calculus is Gentzen's standard sequent calculus (Sequenzenkalkul, literally "calculus of sequences") for classical first-order logic. The letter K stands for the German word klassisch [1].
A sequent is an expression of the form
where and are finite (possibly empty) sequences of formulas (of some language). is called the antecedent, while is the succedent.
Intuitively, the idea behind a sequent is that if all of the formulas in the antecedent hold, then at least one of the formula in the succedent holds. That is, if and , then holds iff
holds.
The inference rules
Weakening
Contraction
Exchange
Negation
Conjunction
Disjunction
todohttps://builds.openlogicproject.org/content/first-order-logic/sequent-calculus/sequent-calculus.pdf Bibliography