Namespaces
Variants
Actions

Difference between revisions of "Sequent (in logic)"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
Line 1: Line 1:
 +
{{TEX|done}}
 
An expression of the form
 
An expression of the form
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845901.png" /></td> </tr></table>
+
$$A_1,\ldots,A_n\to B_1,\ldots,B_m,$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845902.png" /> are formulas. It is read as follows. Under the assumptions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845903.png" />, at least one of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845904.png" /> holds. The part of the sequent on the left of the arrow is called the antecedent, and the part on the right the succedent (consequent). The formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845905.png" /> (note that an empty conjunction denotes truth, and an empty disjunction denotes falsity) is called the formula image of the sequent.
+
where $A_1,\ldots,A_n,B_1,\ldots,B_m$ are formulas. It is read as follows. Under the assumptions $A_1,\ldots,A_n$, at least one of $B_1,\ldots,B_m$ holds. The part of the sequent on the left of the arrow is called the antecedent, and the part on the right the succedent (consequent). The formula $(A_1\&\ldots\&A_n)\supseteq(B_1\lor\ldots\lor B_m)$ (note that an empty conjunction denotes truth, and an empty disjunction denotes falsity) is called the formula image of the sequent.
  
  
Line 10: Line 11:
 
Some authors (particularly those working in the context of constructive logic) restrict the term  "sequent"  to mean an expression of the form
 
Some authors (particularly those working in the context of constructive logic) restrict the term  "sequent"  to mean an expression of the form
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845906.png" /></td> </tr></table>
+
$$A_1,\ldots,A_n\to B,$$
  
i.e. the particular case <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s084/s084590/s0845907.png" /> of the above definition.
+
i.e. the particular case $m=1$ of the above definition.
  
 
For a discussion of Gentzen's sequent calculi cf. [[Gentzen formal system|Gentzen formal system]]; [[Sequent calculus|Sequent calculus]] and, e.g., [[#References|[a2]]].
 
For a discussion of Gentzen's sequent calculi cf. [[Gentzen formal system|Gentzen formal system]]; [[Sequent calculus|Sequent calculus]] and, e.g., [[#References|[a2]]].

Revision as of 21:09, 17 July 2014

An expression of the form

$$A_1,\ldots,A_n\to B_1,\ldots,B_m,$$

where $A_1,\ldots,A_n,B_1,\ldots,B_m$ are formulas. It is read as follows. Under the assumptions $A_1,\ldots,A_n$, at least one of $B_1,\ldots,B_m$ holds. The part of the sequent on the left of the arrow is called the antecedent, and the part on the right the succedent (consequent). The formula $(A_1\&\ldots\&A_n)\supseteq(B_1\lor\ldots\lor B_m)$ (note that an empty conjunction denotes truth, and an empty disjunction denotes falsity) is called the formula image of the sequent.


Comments

Some authors (particularly those working in the context of constructive logic) restrict the term "sequent" to mean an expression of the form

$$A_1,\ldots,A_n\to B,$$

i.e. the particular case $m=1$ of the above definition.

For a discussion of Gentzen's sequent calculi cf. Gentzen formal system; Sequent calculus and, e.g., [a2].

References

[a1] W. Hodges, "Elementary predicate logic" D. Gabbay (ed.) F. Guenther (ed.) , Handbook of philosophical logic , I , Reidel (1983) pp. 1–131
[a2] G. Sundholm, "Systems of deduction" D. Gabbay (ed.) F. Guenther (ed.) , Handbook of philosophical logic , I , Reidel (1983) pp. 133–188, §3
How to Cite This Entry:
Sequent (in logic). Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Sequent_(in_logic)&oldid=17638
This article was adapted from an original article by G.E. Mints (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article