 As the notation makes clear, we use the same shortcuts in formulations involving the regular turnstile (⊢) as for the current variant (≻), despite the difference in role played by these two symbols: the former is a metalinguistic predicate and the latter a device for separating the two sides of a sequent. (“≻”, arranging formulas into sequents, is, as Lemmon (1965) says of his corresponding notation, the formal analogue of the word “therefore”, which arranges sentences into arguments. The former is, by contrast, for making comments about such arguments—for example to the effect that they are valid. Of course there is a little slack in the analogy for Set-Fmla, since we allow the case where there are no premisses.) Any collection Σ of sequents which is closed under the structural rules above gives rise to a corresponding (finitary) consequence relation: Γ ⊢Σ φ iff for some finite Γ0 ⊆ Γ, we have Γ0≻ φ ∈ Σ. We should also have a sequent-based analogue of the notion of a valuation’s being consistent with a consequence relation; accordingly we say that a sequent Γ ≻ φ holds on the valuation v just in case we do not have v(ψ) = T for each ψ ∈ Γ while also v(φ) = F. (When Γ is empty, the sequent holds on v just in case v(φ) = T. It would be uncouth to speak of a sequent as being true on a valuation, however, just as one would not speak of the truth of an argument. Such usages are on a par with, and closely allied to, the mistaken conception of ≻ as a kind of connective.)