Any weakening that appears in a derivation can then be performed right at the start. This may be a convenient change when constructing proofs bottom-up. Independent of these one may also change the way in which contexts are split within the rules: In the cases , and the left context is somehow split into and when going upwards. Since contraction allows for the duplication of these, one may assume that the full context is used in both branches of the derivation. By doing this, one assures that no important premises are lost in the wrong branch. Using weakening, the irrelevant parts of the context can be eliminated later. Absurdity One can introduce , the absurdity constant representing false, with the axiom: Or if, as described above, weakening is to be an admissible rule, then with the axiom: With , negation can be subsumed as a special case of implication, via the definition . Substructural logics Alternatively, one may restrict or forbid the use of some of the structural rules. This yields a variety of substructural logic systems. They are generally weaker than LK (i.e., they have fewer theorems), and thus not complete with respect to the standard semantics of first-order logic. However, they have other interesting properties that have led to applications in theoretical computer science and artificial intelligence. Intuitionistic sequent calculus: System LJ Surprisingly, some small changes in the rules of LK suffice to turn it into a proof system for intuitionistic logic. To this end, one has to restrict to sequents with at most one formula on the right-hand side, and modify the rules to maintain this invariant. For example, is reformulated as follows (where C is an arbitrary formula): The resulting system is called LJ. It is sound and complete with respect to intuitionistic logic and admits a similar cut-elimination proof. This can be used in proving disjunction and existence properties. In fact, the only rules in LK that need to be restricted to single-formula consequents are , (which can be seen as a special case of , as described above) and . When multi-formula consequents are interpreted as disjunctions, all of the other inference rules of LK are derivable in LJ, while the rules and become and (when does not occur free in the bottom sequent) These rules are not intuitionistically valid. See also Cirquent calculus Nested sequent calculus Resolution (logic) Proof theory Notes References External