Stergios Chatzikyriakidis - Formal Semantics in Modern Type Theories

39 33Note that MTT-semantics itself is still denotational (and model-theoretic – see below) in the sense that the meaning of a natural language phrase/sentence is given by its denotation in an MTT, not directly by proof rules, although its foundational languages have a proof-theoretic meaning theory, as described above in the sense of “logical inferentialism” or “proof-theoretic semantics” (Kahle and Schroeder-Heister 2006). Can we extend logical inferentialism to natural language? For example, Francez and his colleagues (Francez 2015) have studied natural language semantics in a way that directly adopts the methodology of proof-theoretic semantics for logical systems and applies it to natural language. However, in order for such semantics to be adequate or viable for natural language, one would have to answer some difficult questions. For example, for a logical language, logicians have recognized that, to capture the meaning of a formula in the use theory, it is central for us to spell out two aspects of its use – how to prove it and how to derive consequences from it, as captured by introduction and elimination rules, respectively. Could this be generalized directly to natural language? This would be a big leap and, unfortunately, a convincing justification has not been forthcoming. In fact, philosophers such as Brandom who advocate “general inferentialism” do not restrict the rule patterns in this way as the following remark by Peregrin (2013) explains:... It is important to realize that this logical kind of inferentialism must be classified as a special case of general inferentialism not just 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 34An 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 35Historically, 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.

Текст предоставлен ООО «ЛитРес».

Прочитайте эту книгу целиком, купив полную легальную версию на ЛитРес.

Безопасно оплатить книгу можно банковской картой Visa, MasterCard, Maestro, со счета мобильного телефона, с платежного терминала, в салоне МТС или Связной, через PayPal, WebMoney, Яндекс.Деньги, QIWI Кошелек, бонусными картами или другим удобным Вам способом.