Editing Sequent (section)

=== 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}}.