In formal logic, a sequent, written using notation like $P_1,\ldots,P_n\vdash C$, expresses the notion that the conclusion $C$ follows from the premises $P_1,\ldots,P_n$. A sequent might be derivable or not, and one can look for particular derivations that result in the sequent, etc.

This class is a data structure for holding a sequent whose premises and conclusion are all LogicConcepts. It does not provide any formal way to assess whether the sequent is valid; such tools are left to other functionality in the Validation module. But it is useful to have this class because the construction of a sequent is a rather technical thing to get right, and compartmentalizing all of those technicalities into one file is good code organization.

Specifically, given a claim, one might try to form a sequent from it by just computing its list of accessibles. However, there are several reasons why this does not always result in the correct set of LogicConcepts. None of these is deep or meaningful; all are somewhat annoying technicalities whose handling we factor into the tools in this class so that we might ignore it elsewhere. All notation used below is putdown.

1. In a BindingEnvironment, say (x y) , { A B }, there is a body (the last child) and there are bound symbols (the children preceding the last). In this case, the children of the BindingEnvironment are x, y, and { A B }. Thus if we considered what's accessible to B, we would find both x and y, even though neither is a proposition, nor is it "citable" at B. Thus we would want to remove the bound variables of BindingEnvironments from consideration when forming a sequent.
2. Support for declared variables already exists in our class hierarchy, even though (at the time of this writing) it is not yet supported in our validation tools. But when it is, we will want to reduce the contents of some premises to remove unusable children from them. For example, if $E$ is an environment that begins with premise $P$ and later contains a claim $C$, we expect $E$ to mean at least { :P C }. However, if inside $E$ we declare $c$ to be a constant and thereafter prove several facts about $c$, including, say, $Q(c)$, then we would not expect the meaning of $E$ to include { :P Q(c) }, because the scope of $c$ ends at the end of $E$. So when adding $E$ to the premise list for a sequent, we will need to modify it to remove conclusions that cannot be safely "exported" from $E$.
3. When we later add support for document dependencies, one possibility is to include dependencies as attributes of the document. But that would put them nowhere in the document's parent/child hierarchy, and thus they would not ever show up as accessible to any LogicConcept. Of course, they should be accessible to every LogicConcept in the document, so a sequent should know to add dependency content to its premise list.

As a consequence of all this, a sequent does not store the original LogicConcept instances from the context in which it was created; it must make copies so that it can modify them in (zero or more of) the ways described above.

Furthemore, the original copies of the LogicConcept instances accessible to a given conclusion may have extraneous attributes that are not relevant to validation (and indeed might confound validation if they were left in place). Thus this class, when making copies of LogicConcepts, also removes any unneeded attributes from them. It also ensures that all premises are marked as givens, and the conclusion is not marked as a given, because a sequent has one item in positive position (the conclusion) and $n-1$ items in negative position (the premises).

Again, all of these little details are technicalities that must be handled, but that are not very conceptually interesting. So we lump the handling of them all into this one class. The end result is stored as a single Environment whose children are the contents of the sequent, { :P_1 ... :P_n C }, with the premises marked given and the conclusion not marked given, with all of the above manipulations already applied.