Sequent calculus
More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms.
Hilbert-style systems typically have a very small number of inference rules, relying more on sets of axioms.
The first sequent calculi systems, LK and LJ, were introduced in 1934/1935 by Gerhard Gentzen[1] as a tool for studying natural deduction in first-order logic (in classical and intuitionistic versions, respectively).
Gentzen further demonstrated the power and flexibility of this technique a few years later, applying a cut-elimination argument to give a (transfinite) proof of the consistency of Peano arithmetic, in surprising response to Gödel's incompleteness theorems.
Since this early work, sequent calculi, also called Gentzen systems,[4][5][6][7] and the general concepts relating to them, have been widely applied in the fields of proof theory, mathematical logic, and automated deduction.
A Hilbert-style system needs no distinction between formulas and judgments; we make one here solely for comparison with the cases that follow.
The price paid for the simple syntax of a Hilbert-style system is that complete formal proofs tend to get extremely long.
In other words, a judgment consists of a list (possibly empty) of formulas on the left-hand side of a turnstile symbol "
At first sight, this extension of the judgment form may appear to be a strange complication—it is not motivated by an obvious shortcoming of natural deduction, and it is initially confusing that the comma seems to mean entirely different things on the two sides of the turnstile.
This means that a symmetry such as De Morgan's laws, which manifests itself as logical negation on the semantic level, translates directly into a left–right symmetry of sequents—and indeed, the inference rules in sequent calculus for dealing with conjunction (∧) are mirror images of those dealing with disjunction (∨).
Many logicians feel [citation needed] that this symmetric presentation offers a deeper insight in the structure of the logic than other styles of proof system, where the classical duality of negation is not as apparent in the rules.
[17] Then he said that in addition to these reasons, the sequent calculus with multiple succedent formulas is intended particularly for his principal theorem ("Hauptsatz").
"[19] Sequent calculus can be seen as a tool for proving formulas in propositional logic, similar to the method of analytic tableaux.
[21] Hence one moves to the following sequent: Again the right hand side includes an implication, whose premise can further be assumed so that only its conclusion needs to be proven: Since the arguments in the left-hand side are assumed to be related by conjunction, this can be replaced by the following: This is equivalent to proving the conclusion in both cases of the disjunction on the first argument on the left.
[23] Starting with any formula in propositional logic, by a series of steps, the right side of the turnstile can be processed until it includes only atomic symbols.
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.
Although stated in a formal way, the above rules allow for a very intuitive reading in terms of classical logic.
Instead of viewing the rules as descriptions for legal derivations in predicate logic, one may also consider them as instructions for the construction of a proof for a given statement.
This reflects the fact that the usual language of first-order logic does not include the "is not implied by" connective
Note that the converse is not true, and its falsity can be seen when attempting to derive it bottom-up, because an existing free variable cannot be used in substitution in the rules
A common simplification involves the use of multisets of formulas in the interpretation of the sequent, rather than sequences, eliminating the need for an explicit permutation rule.
This corresponds to shifting commutativity of assumptions and derivations outside the sequent calculus, whereas LK embeds it within the system itself.
Contraction (C) and Permutation (P) assure that neither the order (P) nor the multiplicity of occurrences (C) of elements of the sequences matters.
This system of rules can be shown to be both sound and complete with respect to first-order logic, i.e. a statement
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.
Surprisingly, some small changes in the rules of LK suffice to turn it into a proof system for intuitionistic logic.
[27] To this end, one has to restrict to sequents with at most one formula on the right-hand side,[28] and modify the rules to maintain this invariant.
It is sound and complete with respect to intuitionistic logic and admits a similar cut-elimination proof.
