Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis

because it is restricted to logical constants, but also because strict constraints are posed on the inferential patterns that can constitute the (meanings of the) logical constants. By contrast, general inferentialism only claims that the meaning of a word is its role vis-à-vis an inferential pattern; there is no claim that each word must have its own constitutive inferential pattern, let alone a claim that this pattern must be of a shape prescribed by Gentzen.In other words, the meaning of an NL phrase/sentence may not be captured by only introduction and elimination rules and there is a good reason for us to be pessimistic for the viability of such an approach.

      40 34 An exception is (Ranta 2015, p. 346) where Ranta pointed out that it is a misunderstanding to think that formal semantics based on Martin-Löf’s type theory (an MTT) is not model-theoretic.

      41 35 Historically, signatures have been used in describing algebraic structures and, for example, more recently they were used in describing many-sorted structures in the study of algebraic specifications (Goguen and Burstall 1983). However, it should be noted that the notion of signature in type theory is rather different from that in algebras, although they may be related informally.