duplicate copies within the left and the right sequences. (However, , 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 ' ' is often referred to as the "turnstile", "right tack", "tee", "assertion sign" or "assertion symbol". It is often read, suggestively, as "yields", "proves" or "entails". Properties Effects of inserting and removing propositions Since every formula in the antecedent (the left side) must be true to conclude the truth of at least one formula in the succedent (the right side), adding formulas to either side results in a weaker sequent, while removing them from either side gives a stronger one. This is one of the symmetry advantages which follows from the use of disjunctive semantics on the right hand side of the assertion symbol, whereas conjunctive semantics is adhered to on the left hand side. 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, ' ⊢ B1, B2 ' means that either B1, or B2, or both must be true. An empty antecedent formula list is equivalent to the "always true" proposition, called the "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 impossible. This is signified by the 'always false' proposition, called the "falsum", denoted "⊥". Since the consequence is false, at least one of the antecedents must be false. Thus for example, ' A1, A2 ⊢ ' means that at least one of the antecedents A1 and A2 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 "not satisfiable". In this case, the meaning of the sequent is effectively '