The sign ⊦ was used by Frege to put in front of sentences that are being asserted as true, as opposed to sentences that are involved in some process of reasoning, but are not themselves put forward as true. This use was superseded in modern logic by the use of the sign to denote the provability relation within a system. {A₁…A_n} ⊦ B means that B may be proved from the premises {A₁…A_n}. ⊦ B means that B may be proved from no assumptions at all, i.e. is a theorem of the system.