 The PTS programme as a theory of meaning can be described as follows: … Replace the received approach of taking sentential meanings as truth-conditions … by taking them as canonical derivability conditions … within a “dedicated” meaning-conferring natural-deduction proof-system in which the derivability conditions are formulated. … The proof system should reflect the “use” of the sentences (their inferential roles) …, and should allow recovering pre-theoretic properties of the meanings of sentences, such as entailment and consequence drawing (inference). … Such a system has two kinds of rules: Introduction rules [and] Elimination rules.