other axiomatizations of propositional calculus, such as Frege's propositional calculus or Jan Łukasiewicz's axiomatization (itself a part of the standard Hilbert system): Every formula that can be proven in these has a reduction tree. This can be shown as follows: Every proof in propositional calculus uses only axioms and the inference rules. Each use of an axiom scheme yields a true logical formula, and can thus be proven in sequent calculus; examples for these are shown below. The only inference rule in the systems mentioned above is modus ponens, which is implemented by the cut rule. The system LK This section introduces the rules of the sequent calculus LK (standing for Logistische Kalkül) as introduced by Gentzen in 1934. A (formal) proof in this calculus is a sequence of sequents, where each of the sequents is derivable from sequents appearing earlier in the sequence by using one of the rules below. Inference rules The following notation will be used: known as the turnstile, separates the assumptions on the left from the propositions on the right and denote formulae of first-order predicate logic (one may also restrict this to propositional logic), , and are finite (possibly empty) sequences of formulae (in fact, the order of formulae does not matter; see ), called contexts, when on the left of the , the sequence of formulas is considered conjunctively (all assumed to hold at the same time), while on the right of the , the sequence of formulas is considered disjunctively (at least one of the formulas must hold for any assignment of variables), denotes an arbitrary term, and denote variables. a variable is said to occur free within a formula if it is not bound by quantifiers or . denotes the formula that is obtained by substituting the term for every free occurrence of the variable in formula with the restriction that the term must be free for the variable in (i.e., no occurrence of any variable in becomes bound in ). , , , , , : These six stand for the two versions of each of three structural rules; one for use on the left ('L') of a , and the other on its right ('R'). The rules are abbreviated 'W' for Weakening (Left/Right), 'C' for Contraction, and 'P' for Permutation. Note that, contrary to the rules for proceeding along the reduction tree presented above, the following rules are for