Editing Sequent (section)

== Interpretation ==

=== History of the meaning of sequent assertions ===
The assertion symbol in sequents originally meant exactly the same as the implication operator. But over time, its meaning has changed to signify provability within a theory rather than semantic truth in all models.

In 1934, Gentzen did not define the assertion symbol ' ⊢ ' in a sequent to signify provability. He defined it to mean exactly the same as the implication operator ' ⇒ '. Using ' → ' instead of ' ⊢ ' and ' ⊃ ' instead of ' ⇒ ', he wrote: "The sequent A<sub>1</sub>, ..., A<sub>μ</sub> → B<sub>1</sub>, ..., B<sub>ν</sub> signifies, as regards content, exactly the same as the formula (A<sub>1</sub> &amp; ... &amp; A<sub>μ</sub>) ⊃ (B<sub>1</sub> ∨ ... ∨ B<sub>ν</sub>)".<ref>{{harvnb|Gentzen|1934|p=180}}.
: 2.4. Die Sequenz A<sub>1</sub>, ..., A<sub>μ</sub> → B<sub>1</sub>, ..., B<sub>ν</sub> bedeutet inhaltlich genau dasselbe wie die Formel
::: (A<sub>1</sub> &amp; ... &amp; A<sub>μ</sub>) ⊃ (B<sub>1</sub> ∨ ... ∨ B<sub>ν</sub>).</ref> (Gentzen employed the right-arrow symbol between the antecedents and consequents of sequents. He employed the symbol ' ⊃ ' for the logical implication operator.)

In 1939, [[David Hilbert|Hilbert]] and [[Paul Bernays|Bernays]] stated likewise that a sequent has the same meaning as the corresponding implication formula.<ref>{{harvnb|Hilbert|Bernays|1970|p=385}}.
: Für die inhaltliche Deutung ist eine Sequenz
::: A<sub>1</sub>, ..., A<sub>r</sub> → B<sub>1</sub>, ..., B<sub>s</sub>,
: worin die Anzahlen r und s von 0 verschieden sind, gleichbedeutend mit der Implikation
::: (A<sub>1</sub> &amp; ... &amp; A<sub>r</sub>) → (B<sub>1</sub> ∨ ... ∨ B<sub>s</sub>)
</ref>

In 1944, [[Alonzo Church]] emphasized that Gentzen's sequent assertions did not signify provability.

: "Employment of the deduction theorem as primitive or derived rule must not, however, be confused with the use of ''Sequenzen'' by Gentzen. For Gentzen's arrow, →, is not comparable to our syntactical notation, ⊢, but belongs to his object language (as is clear from the fact that expressions containing it appear as premisses and conclusions in applications of his rules of inference)."<ref>{{harvnb|Church|1996|p=165}}.</ref>

Numerous publications after this time have stated that the assertion symbol in sequents does signify provability within the theory where the sequents are formulated. [[Haskell Curry|Curry]] in 1963,<ref>{{harvnb|Curry|1977|p=184}}</ref> [[John Lemmon|Lemmon]] in 1965,<ref name=Lemmon1965p12 /> and Huth and Ryan in 2004<ref>{{harvtxt|Huth|Ryan|2004|p=5}}</ref> all state that the sequent assertion symbol signifies provability. However, {{harvtxt|Ben-Ari|2012|p=69}} states that the assertion symbol in Gentzen-system sequents, which he denotes as ' ⇒ ', is part of the object language, not the metalanguage.<ref>{{harvnb|Ben-Ari|2012|p=69}}, defines sequents to have the form ''U'' ⇒ ''V'' for (possibly non-empty) sets of formulas ''U'' and ''V''. Then he writes:
: "Intuitively, a sequent represents 'provable from' in the sense that the formulas in ''U'' are assumptions for the set of formulas ''V'' that are to be proved. The symbol ⇒ is similar to the symbol ⊢ in Hilbert systems, except that ⇒ is part of the object language of the deductive system being formalized, while ⊢ is a metalanguage notation used to reason about deductive systems."</ref>

According to [[Dag Prawitz|Prawitz]] (1965): "The calculi of sequents can be understood as meta-calculi for the deducibility relation in the corresponding systems of natural deduction."<ref>{{harvnb|Prawitz|2006|p=90}}.</ref> And furthermore: "A proof in a calculus of sequents can be looked upon as an instruction on how to construct a corresponding natural deduction."<ref>See {{harvnb|Prawitz|2006|p=91}}, for this and further details of interpretation.</ref> In other words, the assertion symbol is part of the object language for the sequent calculus, which is a kind of meta-calculus, but simultaneously signifies deducibility in an underlying natural deduction system.

=== Intuitive meaning ===
{{Refimprove section|date=June 2014|talk=Assertion symbols in sequents do not signify provability.}}
A sequent is a [[Formalism (mathematics)|formalized]] statement of [[Proof theory|provability]] that is frequently used when specifying [[proof calculus|calculi]] for [[deductive reasoning|deduction]]. In the sequent calculus, the name ''sequent'' is used for the construct, which can be regarded as a specific kind of [[Judgment (mathematical logic)|judgment]], characteristic to this deduction system.

The intuitive meaning of the sequent <math>\Gamma\vdash\Sigma</math> is that under the assumption of Γ the conclusion of Σ is provable. Classically, the formulae on the left of the turnstile can be interpreted [[logical conjunction|conjunctively]] while the formulae on the right can be considered as a [[logical disjunction|disjunction]]. This means that, when all formulae in Γ hold, then at least one formula in Σ also has to be true. If the succedent is empty, this is interpreted as falsity, i.e. <math>\Gamma\vdash</math> means that Γ proves falsity and is thus inconsistent. On the other hand an empty antecedent is assumed to be true, i.e., <math>\vdash\Sigma</math> means that Σ follows without any assumptions, i.e., it is always true (as a disjunction).  A sequent of this form, with Γ empty, is known as a [[logical assertion]].

Of course, other intuitive explanations are possible, which are classically equivalent.  For example, <math>\Gamma\vdash\Sigma</math> can be read as asserting that it cannot be the case that every formula in Γ is true and every formula in Σ is false (this is related to the double-negation interpretations of classical [[intuitionistic logic]], such as [[Glivenko's translation|Glivenko's theorem]]).

In any case, these intuitive readings are only pedagogical. Since formal proofs in proof theory are purely [[syntax|syntactic]], the [[semantics|meaning]] of (the derivation of) a sequent is only given by the properties of the calculus that provides the actual [[rule of inference|rules of inference]].

Barring any contradictions in the technically precise definition above we can describe sequents in their introductory logical form. <math>\Gamma</math> represents a set of assumptions that we begin our logical process with, for example "Socrates is a man" and "All men are mortal". The <math>\Sigma</math> represents a logical conclusion that follows under these premises. For example "Socrates is mortal" follows from a reasonable formalization of the above points and we could expect to see it on the <math>\Sigma</math> side of the ''turnstile''. In this sense, <math>\vdash</math> means the process of reasoning, or "therefore" in English.