Editing Sequent (section)

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