  Proof-theoretic semantics is inherently inferential, as it is inferential activity which manifests itself in proofs. It thus belongs to inferentialism (see Brandom, 2000) according to which inferences and the rules of inference establish the meaning of expressions, in contradistinction to denotationalism, according to which denotations are the primary sort of meaning. Inferentialism and the ‘meaning-as-use’ view of semantics is the broad philosophical framework of proof-theoretic semantics. This general philosophical and semantical perspective merged with constructive views which originated in the philosophy of mathematics, especially in mathematical intuitionism. Most forms of proof-theoretic semantics are intuitionistic in spirit, which means in particular that principles of classical logic such as the law of excluded middle or the double negation law are rejected or at least considered problematic. This is partly due to the fact that the main tool of proof-theoretic semantics, the calculus of natural deduction, is biased towards intuitionistic logic, in the sense that the straightforward formulation of its elimination rules is the intuitionistic one. There classical logic is only available by means of some rule of indirect proof, which, at least to some extent, destroys the symmetry of the reasoning principles (see section  3.5).  If one adopts the standpoint of natural deduction, then intuitionistic logic is a natural logical system. Also the BHK (Brouwer-Heyting-Kolmogorov) interpretation of the logical signs plays a significant role. This interpretation is not a unique approach to semantics, but comprises various ideas which are often more informally than formally described. Of particular importance is its functional view of implication, according to which a proof of A → B is a constructive function which, when applied to a proof of A yields a proof of B. This functional perspective underlies many conceptions of proof-theoretic semantics, in particular those of Lorenzen, Prawitz and Martin Löf (see sections  2.1.1,  2.2.2,  2.2.3).