  The semantics of implication lies at the heart of proof-theoretic semantics. In contradistinction to classical truth-condition semantics, implication is a logical constant in its own right. It has also the characteristic feature that it is tied to the concept of consequence. It can be viewed as expressing consequence at the sentential level due to modus ponens and to what in Hilbert-style systems is called the deduction theorem, i.e. the equivalence of Γ,A ⊢ B and Γ ⊢ A → B.