Editing Sequent (section)

== Introduction ==

=== The form and semantics of sequents ===

Sequents are best understood in the context of the following three kinds of [[Judgment (mathematical logic)|logical judgments]]:
<ol>
<li>'''Unconditional assertion'''. No antecedent formulas.
* Example:  ⊢ ''B''
* Meaning: ''B'' is true.
<li>'''Conditional assertion'''. Any number of antecedent formulas.
<ol type="a">
<li>'''Simple conditional assertion'''. Single consequent formula.
* Example: ''A<sub>1</sub>'', ''A<sub>2</sub>'', ''A<sub>3</sub>'' ⊢ ''B''
* Meaning: IF ''A<sub>1</sub>'' AND ''A<sub>2</sub>'' AND ''A<sub>3</sub>'' are true, THEN ''B'' is true.
<li>'''Sequent'''. Any number of consequent formulas. 
* Example: ''A<sub>1</sub>'', ''A<sub>2</sub>'', ''A<sub>3</sub>'' ⊢ ''B<sub>1</sub>'', ''B<sub>2</sub>'', ''B<sub>3</sub>'', ''B<sub>4</sub>''
* Meaning: IF ''A<sub>1</sub>'' AND ''A<sub>2</sub>'' AND ''A<sub>3</sub>''  are true, THEN ''B<sub>1</sub>'' OR ''B<sub>2</sub>'' OR ''B<sub>3</sub>'' OR ''B<sub>4</sub>'' is true.
</ol>
</ol>
Thus sequents are a generalization of simple conditional assertions, which are a generalization of unconditional assertions.

The word "OR" here is the [[logical disjunction|inclusive OR]].<ref>The disjunctive semantics for the right side of a sequent is stated and explained by {{harvnb|Curry|1977|pp=189–190}}, {{harvnb|Kleene|2002|pp=290, 297}}, {{harvnb|Kleene|2009|p=441}}, {{harvnb|Hilbert|Bernays|1970|p=385}}, {{harvnb|Smullyan|1995|pp=104–105}}, {{harvnb|Takeuti|2013|p=9}}, and {{harvnb|Gentzen|1934|p=180}}.</ref> The motivation for disjunctive semantics on the right side of a sequent comes from three main benefits.
# The symmetry of the classical [[rule of inference|inference rules]] for sequents with such semantics.
# The ease and simplicity of converting such classical rules to intuitionistic rules.
# The ability to prove completeness for predicate calculus when it is expressed in this way.
All three of these benefits were identified in the founding paper by {{harvtxt|Gentzen|1934|p=194}}.

Not all authors have adhered to Gentzen's original meaning for the word "sequent". For example, {{harvtxt|Lemmon|1965}} used the word "sequent" strictly for simple conditional assertions with one and only one consequent formula.<ref name=Lemmon1965p12>{{harvnb|Lemmon|1965|p=12}}, wrote: "Thus a sequent is an argument-frame containing a set of assumptions and a conclusion which is claimed to follow from them. [...] The propositions to the left of '⊢' become assumptions of the argument, and the proposition to the right becomes a conclusion validly drawn from those assumptions."</ref> The same single-consequent definition for a sequent is given by {{harvnb|Huth|Ryan|2004|p=5}}.

=== Syntax details ===
In a general sequent of the form
:<math>\Gamma\vdash\Sigma</math>
both Γ and Σ are [[sequence]]s of logical formulas, not [[set (mathematics)|sets]]. Therefore both the number and order of occurrences of formulas are significant. In particular, the same formula may appear twice in the same sequence. The full set of [[Sequent calculus#Inference rules|sequent calculus inference rules]] contains rules to swap adjacent formulas on the left and on the right of the assertion symbol (and thereby arbitrarily [[Permutation|permute]] the left and right sequences), and also to insert arbitrary formulas and remove duplicate copies within the left and  the right sequences. (However, {{harvtxt|Smullyan|1995|pp=107–108}}, uses ''sets'' of formulas in sequents instead of sequences of formulas. Consequently the three pairs of ''structural rules'' called "thinning", "contraction" and "interchange" are not required.)

The symbol ' <math>\vdash</math> ' is often referred to as the "[[Turnstile (symbol)|turnstile]]", "right tack", "tee", "assertion sign" or "assertion symbol". It is often read, suggestively, as "yields", "proves" or "entails".

=== Properties ===

==== Effects of inserting and removing propositions ====
Since every formula in the antecedent (the left side) must be true to conclude the truth of at least one formula in the succedent (the right side), adding formulas to either side results in a weaker sequent, while removing them from either side gives a stronger one. This is one of the symmetry advantages which follows from the use of disjunctive semantics on the right hand side of the assertion symbol, whereas conjunctive semantics is adhered to on the left hand side.

==== Consequences of empty lists of formulas ====
In the extreme case where the list of ''antecedent'' formulas of a sequent is empty, the consequent is unconditional. This differs from the simple unconditional assertion because the number of consequents is arbitrary, not necessarily a single consequent. Thus for example, ' ⊢ ''B<sub>1</sub>'', ''B<sub>2</sub>'' ' means that either ''B<sub>1</sub>'', or  ''B<sub>2</sub>'', or both must be true. An empty antecedent formula list is equivalent to the "always true" proposition, called the "[[Tautology (logic)|verum]]", denoted "⊤". (See [[Tee (symbol)]].)

In the extreme case where the list of ''consequent'' formulas of a sequent is empty, the rule is still that at least one term on the right  be true, which is clearly [[Contradiction|impossible]]. This is signified by the 'always false' proposition, called the "[[False (logic)|falsum]]", denoted "⊥". Since the consequence is false, at least one of the antecedents must be false. Thus for example, ' ''A<sub>1</sub>'', ''A<sub>2</sub>'' ⊢ ' means that at least one of the antecedents ''A<sub>1</sub>'' and ''A<sub>2</sub>'' must be false.

One sees here again a symmetry because of the disjunctive semantics on the right hand side. If the left side is empty, then one or more right-side propositions must be true. If the right side is empty, then one or more of the left-side propositions must be false.

The doubly extreme case ' ⊢ ', where both the antecedent and consequent lists of formulas are empty is "[[Interpretation (logic)#Non-empty domain requirement|not satisfiable]]".<ref>{{harvnb|Smullyan|1995|p=105}}.</ref> In this case, the meaning of the sequent is effectively ' ⊤ ⊢ ⊥  '. This is equivalent to the sequent ' ⊢ ⊥ ', which clearly cannot be valid.

=== Examples ===
A sequent of the form ' ⊢ α, β ', for logical formulas α and β, means that either α is true or β is true (or both). But it does not mean that either α is a tautology or β is a tautology. To clarify this, consider the example ' ⊢ B ∨ A, C ∨ ¬A '. This is a valid sequent because either B ∨ A is true or C ∨ ¬A is true. But neither of these expressions is a tautology in isolation. It is the ''disjunction'' of these two expressions which is a tautology.

Similarly, a sequent of the form ' α, β ⊢ ', for logical formulas α and β, means that either α is false or β is false. But it does not mean that either α is a contradiction or β is a contradiction. To clarify this, consider the example ' B ∧ A, C ∧ ¬A ⊢ '. This is a valid sequent because either B ∧ A is false or C ∧ ¬A is false. But neither of these expressions is a contradiction in isolation. It is the ''conjunction'' of these two expressions which is a contradiction.

=== Rules ===
Most proof systems provide ways to deduce one sequent from another. These inference rules are written with a list of sequents above and below a [[Coplanarity|line]]. This rule indicates that if everything above the line is true, so is everything under the line.

A typical rule is:

:<math> \frac{\Gamma,\alpha\vdash\Sigma\qquad \Gamma\vdash\alpha}{\Gamma\vdash\Sigma}</math>

This indicates that if we can deduce that <math>\Gamma,\alpha</math> yields <math>\Sigma</math>, and that <math>\Gamma</math> yields <math>\alpha</math>, then we can also deduce that <math>\Gamma</math> yields  <math>\Sigma</math>. (See also the full set of [[sequent calculus#Inference rules|sequent calculus inference rules]].)