Editing Sequent (section)

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