Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis
192
196 193
197 194
198 195
199 196
200 197
201 198
202 199
203 200
204 201
205 202
206 203
207 204
208 205
209 206
210 207
211 209
212 210
213 211
214 212
215 213
216 214
217 215
218 216
219 217
220 218
221 219
222 220
223 221
224 222
225 223
226 225
227 226
228 227
229 228
230 229
231 231
232 232
233 233
234 234
235 235
236 236
Logic Linguistics and Computer Science Set
coordinated by
Christian Retoré
Volume 2
Formal Semantics in Modern Type Theories
Stergios Chatzikyriakidis
Zhaohui Luo
First published 2020 in Great Britain and the United States by ISTE Ltd and John Wiley & Sons, Inc.
Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced, stored or transmitted, in any form or by any means, with the prior permission in writing of the publishers, or in the case of reprographic reproduction in accordance with the terms and licenses issued by the CLA. Enquiries concerning reproduction outside these terms should be sent to the publishers at the undermentioned address:
ISTE Ltd
27-37 St George’s Road
London SW19 4EU
UK
John Wiley & Sons, Inc.
111 River Street
Hoboken, NJ 07030
USA
© ISTE Ltd 2020
The rights of Stergios Chatzikyriakidis and Zhaohui Luo to be identified as the authors of this work have been asserted by them in accordance with the Copyright, Designs and Patents Act 1988.
Library of Congress Control Number: 2020943853
British Library Cataloguing-in-Publication Data
A CIP record for this book is available from the British Library
ISBN 978-1-78630-128-4
Preface
To communicate linguistically is to convey meaning. Semantics is the academic discipline that analyzes meaning. In this book, we study natural language semantics formally in the framework of modern type theories (MTTs). Examples of MTTs include Martin-Löf’s predicative type theory (Martin-Löf 1984; Nordström et al. 1990) and the impredicative type theories – unifying theory of dependent types UTT (Luo 1994) and pCIC (Coq 2010). MTTs offer a foundational framework that was not available in the study of formal semantics until Ranta’s work in the early 1990s when he applied Martin-Löf’s type theory to formal semantics (Ranta 1994). In the past decade, the development of formal semantics in MTTs (MTT-semantics for short) has shown that MTTs are powerful alternatives to, and arguably more advantageous than, Church’s simple type theory (Church 1940) as employed in Montague semantics (Montague 1974).
MTTs have rich type structures and, at the same time, are specified by means of proof-theoretic natural deduction rules. Therefore, they provide powerful tools in formal semantics, on the one hand, and have the appeal of being supported by a proof-theoretic theory of meaning, on the other hand. The former allows one to study a wide range of linguistic features, some of which have proved difficult to describe adequately in the Montagovian setting. The latter not only provides a solid proof-theoretic foundation for MTT-semantics but also leads to practical computer-assisted reasoning tools supported by the existing proof technology. These two aspects can be summarized by saying that MTT-semantics is both model-theoretic and proof-theoretic, a thesis that was put forward by the second author in Luo (2014) and further elaborated in Luo (2019a). This makes MTTs a promising and attractive semantic framework that is unique: such a framework was not available in traditional logical settings and the MTT-framework offers new perspectives on natural language semantics.
Learning MTTs can be laborious. This is partly because MTTs incorporate several new concepts that even traditional logicians may find difficult to comprehend at the beginning, let alone the linguists who apply logics to formal semantics. Therefore, in this book, besides studying MTT-semantics, we shall try our best to introduce the basics of MTTs informally: the explanations will be rigorous with examples from linguistic semantics. It is our hope that this will make it easier to understand and study MTT-semantics.
This book consists of the following seven chapters, where Chapters 1, 2, 3, sections 7.1 and 7.2 are mainly written by Luo, and Chapters 4, 5, 6 and section 7.3 are mainly written by Chatzikyriakidis.
–