Stergios Chatzikyriakidis - Formal Semantics in Modern Type Theories

122 114

123 115

124 116

125 117

126 118

127 119

128 120

129 121

130 122

131 123

132 124

133 125

134 127

135 128

136 129

137 130

138 131

139 132

140 133

141 134

142 135

143 136

144 137

145 138

146 139

147 140

148 141

149 142

150 143

151 144

152 145

153 146

154 147

155 148

156 149

157 150

158 151

159 152

160 153

161 154

162 155

163 156

164 157

165 158

166 159

167 160

168 161

169 162

170 163

171 164

172 165

173 166

174 167

175 168

176 169

177 170

178 171

179 172

180 173

181 175

182 176

183 177

184 178

185 179

186 181

187 182

188 183

189 184

190 185

191 187

192 188

193 189

194 191

195 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

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

www.iste.co.uk

John Wiley & Sons, Inc.

111 River Street

Hoboken, NJ 07030

USA

www.wiley.com

© 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

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.1and 7.2are mainly written by Luo, and Chapters 4, 5, 6and section 7.3are mainly written by Chatzikyriakidis.

– Chapter 1, Type Theories and Semantic Studies, starts with an overview of the historical development of type theories and a discussion on how to use a type theory as a foundational language for formal semantics. We then briefly describe Montague semantics, which is based on simple type theory, 1 and MTT-semantics, and compare them by means of some simple examples. This serves to introduce the basics of MTT-semantics in a very sketchy manner, together with some summary notes on its historical development, and allows us to outline several important merits of employing MTTs as a foundational semantic framework.

– Chapter 2, Modern Type Theories, consists of an informal but rigorous and precise introduction to MTTs, mainly for linguistic semanticists. In order to introduce the basic concepts in MTTs, we use explanatory examples to show how these may be employed in semantic constructions and, in most cases, we present their formal rules in appendices (mainly for completeness). Special attention is paid to several mechanisms that are particularly important for MTT-semantics, including coercive subtyping (Luo 1997), signatures (Luo 2014) and linguistic universes (Luo 2011b; Chatzikyriakidis and Luo 2012). We shall also give a complete formal presentation of the type theories used in this book, which is based on various studies (Luo 2014, 2019a), both for completeness and for reference in future work.

– Chapter 3, Formal Semantics in Modern Type Theories, is a central chapter that explicates several important features of MTT-semantics and shows that the MTT-semantic approach is viable and coherent, on the one hand, and provides flexible and powerful mechanisms for adequate semantic interpretations, on the other hand. Some features are discussed in depth: the CNs-as-types paradigm (Ranta 1994; Luo 2012a), subtyping in MTT-semantics (Luo 2009c, 2012b) and propositional forms of judgmental interpretations (Xue et al. 2018). As a case study for MTT-semantics, we study semantics of adjectival modification according to a traditional classification of adjectives into intersective, subsective, privative and non-committal adjectives, and investigate how such different adjectival modifications can be modeled adequately in the CNs-as-types paradigm. 2 This case study, together with the next two chapters, illustrates how the rich type structure in MTTs provide fruitful tools for modeling various linguistic features.