Abstract
Type theories have been used as foundational languages for formal semantics. Under the propositions-as-types principle, most modern type systems have explicit proof objects which, however, cause problems in obtaining correct identity criteria in semantics. Therefore, it has been proposed that some principle of proof irrelevance should be enforced in order for a type theory to be an adequate semantic language. This paper investigates how proof irrelevance can be enforced, particularly in predicative type systems. In an impredicative type theory such as UTT, proof irrelevance can be imposed directly since the type Prop in such a type theory represents the totality of logical propositions and helps to distinguish propositions from other types. In a predicative type theory, however, such a simple approach would not work; for example, in Martin-Löf’s type theory (MLTT), propositions and types are identified and, hence, proof irrelevance would have implied the collapse of all types. We propose that Martin-Löf’s type theory should be extended with h-logic, as proposed by Veovodsky and studied in the HoTT project, where proof irrelevance is built-in in the notion of logical proposition. This amounts to MLTT\(_h\), a predicative type system that can be adequately employed for formal semantics.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
It may be interesting to remark that, recognising that interpreting CNs as types has several advantages, some researchers have suggested that both paradigms need be considered including, for instance, Retoré’s idea in this respect [35]. A related issue in type-theoretical semantics is how to turn judgemental interpretations into corresponding propositional forms, as studied in [41] which proposes an axiomatic solution for such transformations that can be justified by means of heterogenous equality of type theory.
- 2.
Technically, \(\Sigma \)-types are used—see Sect. 2.2 and Footnote 6 for a further description of \(\Sigma \)-types.
- 3.
PaT stands for ‘propositions as types’.
- 4.
See the second paragraph of the Conclusion section for another potential issue in this respect, but this is out of the scope of the current paper.
- 5.
In general, one may say that an interpretation of a CN should actually be a setoid—a type together with an identity criterion, although in most cases, the situation is more straightforward and can be simplified in that one does not have to mention the identity criterion anymore [7].
- 6.
A \(\Sigma \)-type is an inductive type of dependent pairs. Here is an informal description of the basic laws governing \(\Sigma \)-types (see, for example, [30] for the formal rules and further explanations).
-
If A is a type and B is an A-indexed family of types, then \(\Sigma (A,B)\), or sometimes written as \(\Sigma x{:}\, A.B(x)\), is a type.
-
\(\Sigma (A,B)\) consists of pairs (a, b) such that a is of type A and b is of type B(a).
-
\(\Sigma \)-types are associated projection operations \(\pi _1\) and \(\pi _2\) so that \(\pi _1(a,b)=a\) and \(\pi _2(a,b)=b\), for every (a, b) of type \(\Sigma (A,B)\).
When B(x) is a constant type (i.e., always the same type no matter what x is), the \(\Sigma \)-type degenerates into the product type \(A\times B\) of non-dependent pairs.
-
- 7.
Here, the equality \(=\) is the definitional equality in type theory. In §3, when we consider h-logic, the equality will be the propositional equality. We shall not emphasise the differences of these two equalities in the current paper, partly because it would not affect our understandings of the main issues.
- 8.
A reviewer has asked the question whether ‘one should use impredicative type theories rather than predicative ones for studying logics of natural language’ (and maybe others would ask similar questions.) Some people would have drawn this conclusion and, in particular, those (including the author himself) who do not think that impredicativity is problematic would have agreed so. However, some others may think otherwise, believing that impredicativity is problematic in foundations of mathematics (or even in general); if so, predicative type theories would then have their merits and should be considered.
- 9.
Thanks to Justyna Grudziñska for a discussion about this example.
- 10.
For people who are familiar with type theory, this implies that canonicity fails to hold for the resulting type theory.
- 11.
Of course, we recognise that MLTT\(_h\) is a proper extension of MLTT, although this seems to be the best one could do (but further research may be needed to see whether it is possible to do otherwise).
- 12.
Although the current work has not been published until now, its idea, i.e., using HoTT’s h-logic instead of the PaT logic, has been in the author’s mind for a long time. This has partly contributed to the decision of including Martin-Löf’s type theory as one of the MTTs for MTT-semantics.
References
Agda.: The Agda proof assistant (developed at Chalmers, Sweden) (2008). http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php
Baker, M.: Lexical Categories: verbs, Nouns and Adjectives, vol. 102. Cambridge University Press, Cambridge (2003)
Bekki, D.: Representing anaphora with dependent types. LACL 2014, LNCS 8535 (2014)
Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill (1967)
Boldini, P.: Formalizing context in intuitionistic type theory. Fundam. Inform. 42(2), 1–23 (2000)
Callaghan, P., Luo, Z.: An implementation of LF with coercive subtyping and universes. J. Autom. Reason. 27(1), 3–27 (2001)
Chatzikyriakidis, S., Luo, Z.: Identity criteria of common nouns and dot-types for copredication. Oslo Stud. Lang. 10(2) (2018)
Chatzikyriakidis, S., Luo, Z.: Formal Semantics in Modern Type Theories. Wiley & ISTE Science Publishing Ltd., (2019) (to appear)
Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(1) (1940)
Cooper, R.: Records and record types in semantic theory. J. Log. Comput. 15(2) (2005)
Curry, H.B., Feys, R.: Combinatory Logic, vol. 1. North Holland Publishing Company (1958)
Dapoigny, R., Barlatier, P.: Modeling contexts with dependent types. Fundam. Inform. 21 (2009)
Frege, G.: Grundlagen der Arithmetik. Basil Blackwell (Translation by J. Austin in 1950: The Foundations of Arithmetic) (1884)
Gallin, D.: Intensional and higher-order modal logic: with applications to Montague semantics (1975)
Geach, P.: Reference and Generality. Cornell University Press (1962)
Groenendijk, J., Stokhof, M.: Dynamic predicate logic. Linguist. Philos. 14, 1 (1991)
Grudzińska, J., Zawadowski, M.: Generalized quantifiers on dependent types: a system for anaphora. In: Chatzikyriakidis, S., Luo, Z. (eds.). Modern Perspectives in Type-Theoretical Semantics (2017)
Gupta, A.: The Logic of Common Nouns. Yale University Press (1980)
Heim, I.: File change semantics and the familiarity theory of definiteness. In: Bäuerle, R. et al. (eds.) Meaning, Use and Interpretation of Language (1983)
Howard, W.A.: The formulae-as-types notion of construction. In: Hindley, J., Seldin, J. (eds.). To H. B. Curry: Essays on Combinatory Logic. Academic Press (1980)
Kamp, H.: A theory of truth and semantic representation. In: Groenendijk, J. et al. (eds.). Formal Methods in the Study of Language (1981)
Luo, Z.: Computation and Reasoning: a Type Theory for Computer Science. Oxford University Press (1994)
Luo, Z.: Type-theoretical semantics with coercive subtyping. Semantics and Linguistic Theory 20 (SALT20), Vancouver (2010)
Luo, Z.: Common nouns as types. In: Bechet, D., Dikovsky, A. (eds.). Logical Aspects of Computational Linguistics (LACL’2012). LNCS 7351 (2012)
Luo, Z.: Formal semantics in modern type theories with coercive subtyping. Linguist. Philos. 35(6), 491–513 (2012)
Luo, Z.: Formal semantics in modern type theories: is it model-theoretic, proof-theoretic, or both?. In: Invited talk at Logical Aspects of Computational Linguistics 2014 (LACL 2014), vol. 8535, pp. 177–188, Toulouse. LNCS (2014)
Luo, Z., Callaghan, P.: Coercive subtyping and lexical semantics (extended abstract). LACL’98 (extended abstracts), available in request to the first author or as. http://www.cs.rhul.ac.uk/home/zhaohui/LACL98.abstract.ps (1998)
Luo, Z., Pollack, R.: LEGO proof development system: user’s manual. LFCS Report ECS-LFCS-92-211, Dept of Computer Science, Univ of Edinburgh (1992)
Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Rose, H., Shepherdson, J.C. (eds.). Logic Colloquium’73 (1975)
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)
Moltmann, F.: Unbound anaphoric pronouns: E-type, dynamic and atructured-propositions approaches. Synthese 153 (1983)
Montague, R.: Formal Philosophy. R. Yale University Press, Collected papers edited by Thomason (1974)
Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf’s type theory: an introduction. Oxford University Press (1990)
Ranta, A.: Type-theoretical Grammar. Oxford University Press (1994)
Retoré, C.: The Montagovian generative lexicon \(\lambda \)Ty\(_n\): a type theoretical framework for natural language semantics. In: Matthes, R., Schubert, A. (eds.). Proceedings of the TYPES2013 (2013)
Sundholm, G.: Proof theory and meaning. Gabbay, D., Guenthner, F. (eds.). Handbook of Philosophical Logic, vol. III (1986)
Sundholm, G.: Constructive generalized quantifiers. Synthese 79(1), 1–12 (1989)
Tanaka, R.: Generalized quantifiers in dependent type semantics. Talk given at Ohio State University (2015)
The Coq Development Team: The Coq Proof Assistant Reference Manual (Version 8.0), INRIA (2004)
The Univalent Foundations Program: Homotopy type theory: univalent foundations of mathematics. Technical report, Institute for Advanced Study (2013)
Xue, T., Luo, Z., Chatzikyriakidis, S.: Propositional forms of judgemental interpretations. In: Proceedings of the Workshop on Natural Language and Computer Science, Oxford (2018)
Acknowledgements
Partially supported by EU COST Action EUTYPES (CA15123, Research Network on Types).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Luo, Z. (2020). Proof Irrelevance in Type-Theoretical Semantics. In: Loukanova, R. (eds) Logic and Algorithms in Computational Linguistics 2018 (LACompLing2018). Studies in Computational Intelligence, vol 860. Springer, Cham. https://doi.org/10.1007/978-3-030-30077-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-30077-7_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30076-0
Online ISBN: 978-3-030-30077-7
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)