In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in first-order logic (in classical and intuitionistic versions, respectively). Gentzen's so-called "Main Theorem" (Hauptsatz) about LK and LJ was the cut-elimination theorem, a result with far-reaching meta-theoretic consequences, including consistency. 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) and the general concepts relating to them have been widely applied in the fields of proof theory, mathematical logic, and automated deduction.
Other articles related to "sequent calculus, sequent, sequents, calculus":
... theorem (or Gentzen's Hauptsatz) is the central result establishing the significance of the sequent calculus ... The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus that makes use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut ... A sequent is a logical expression relating multiple sentences, in the form "", which is to be read as "A, B, C, proves N, O, P", and (as glossed by Gentzen) should be understood as ...
... To this end, one has to restrict to sequents with exactly one formula on the right-hand side, and modify the rules to maintain this invariant ...
... correspondence can be settled for the formalism known as Gentzen's sequent calculus but it is not a correspondence with a well-defined pre-existing model of computation as it was for Hilbert-style and ... Sequent calculus is characterized by the presence of left introduction rules, right introduction rule and a cut rule that can be eliminated ... The structure of sequent calculus relates to a calculus whose structure is close to the one of some abstract machines ...
... Propositional calculus is commonly organized as a Hilbert system, whose operations are just those of Boolean algebra and whose theorems are Boolean tautologies, those Boolean terms equal to the Boolean constant 1 ... Another form is sequent calculus, which has two sorts, propositions as in ordinary propositional calculus, and pairs of lists of propositions called sequents, such as A∨B, A∧C,… A ... The two halves of a sequent are called the antecedent and the succedent respectively ...
Famous quotes containing the words calculus and/or sequent:
“I try to make a rough music, a dance of the mind, a calculus of the emotions, a driving beat of praise out of the pain and mystery that surround me and become me. My poems are meant to make your mind get up and shout.”
—Judith Johnson Sherwin (b. 1936)
“Nor sequent centuries could hit
Orbit and sum of SHAKSPEAREs wit.
The men who lived with him became
Poets, for the air was fame.”
—Ralph Waldo Emerson (18031882)