Skip to main content
SpringerLink
Log in

Proof Irrelevance in Type-Theoretical Semantics

  • Chapter
  • First Online:
Book cover Logic and Algorithms in Computational Linguistics 2018 (LACompLing2018)

Part of the book series: Studies in Computational Intelligence ((SCI,volume 860))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 119.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 159.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 159.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 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. 2.

    Technically, \(\Sigma \)-types are used—see Sect. 2.2 and Footnote 6 for a further description of \(\Sigma \)-types.

  3. 3.

    PaT stands for ‘propositions as types’.

  4. 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. 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. 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. 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. 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. 9.

    Thanks to Justyna Grudziñska for a discussion about this example.

  10. 10.

    For people who are familiar with type theory, this implies that canonicity fails to hold for the resulting type theory.

  11. 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. 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

  1. Agda.: The Agda proof assistant (developed at Chalmers, Sweden) (2008). http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php

  2. Baker, M.: Lexical Categories: verbs, Nouns and Adjectives, vol. 102. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  3. Bekki, D.: Representing anaphora with dependent types. LACL 2014, LNCS 8535 (2014)

    Google Scholar 

  4. Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill (1967)

    Google Scholar 

  5. Boldini, P.: Formalizing context in intuitionistic type theory. Fundam. Inform. 42(2), 1–23 (2000)

    MathSciNet  MATH  Google Scholar 

  6. Callaghan, P., Luo, Z.: An implementation of LF with coercive subtyping and universes. J. Autom. Reason. 27(1), 3–27 (2001)

    Article  MathSciNet  Google Scholar 

  7. Chatzikyriakidis, S., Luo, Z.: Identity criteria of common nouns and dot-types for copredication. Oslo Stud. Lang. 10(2) (2018)

    Google Scholar 

  8. Chatzikyriakidis, S., Luo, Z.: Formal Semantics in Modern Type Theories. Wiley & ISTE Science Publishing Ltd., (2019) (to appear)

    Google Scholar 

  9. Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(1) (1940)

    Article  MathSciNet  Google Scholar 

  10. Cooper, R.: Records and record types in semantic theory. J. Log. Comput. 15(2) (2005)

    Article  MathSciNet  Google Scholar 

  11. Curry, H.B., Feys, R.: Combinatory Logic, vol. 1. North Holland Publishing Company (1958)

    Google Scholar 

  12. Dapoigny, R., Barlatier, P.: Modeling contexts with dependent types. Fundam. Inform. 21 (2009)

    Google Scholar 

  13. Frege, G.: Grundlagen der Arithmetik. Basil Blackwell (Translation by J. Austin in 1950: The Foundations of Arithmetic) (1884)

    Google Scholar 

  14. Gallin, D.: Intensional and higher-order modal logic: with applications to Montague semantics (1975)

    Chapter  Google Scholar 

  15. Geach, P.: Reference and Generality. Cornell University Press (1962)

    Google Scholar 

  16. Groenendijk, J., Stokhof, M.: Dynamic predicate logic. Linguist. Philos. 14, 1 (1991)

    Google Scholar 

  17. 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)

    Google Scholar 

  18. Gupta, A.: The Logic of Common Nouns. Yale University Press (1980)

    Google Scholar 

  19. 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)

    Google Scholar 

  20. 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)

    Google Scholar 

  21. Kamp, H.: A theory of truth and semantic representation. In: Groenendijk, J. et al. (eds.). Formal Methods in the Study of Language (1981)

    Google Scholar 

  22. Luo, Z.: Computation and Reasoning: a Type Theory for Computer Science. Oxford University Press (1994)

    Google Scholar 

  23. Luo, Z.: Type-theoretical semantics with coercive subtyping. Semantics and Linguistic Theory 20 (SALT20), Vancouver (2010)

    Google Scholar 

  24. Luo, Z.: Common nouns as types. In: Bechet, D., Dikovsky, A. (eds.). Logical Aspects of Computational Linguistics (LACL’2012). LNCS 7351 (2012)

    Google Scholar 

  25. Luo, Z.: Formal semantics in modern type theories with coercive subtyping. Linguist. Philos. 35(6), 491–513 (2012)

    Article  Google Scholar 

  26. 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)

    Google Scholar 

  27. 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)

  28. 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)

    Google Scholar 

  29. Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Rose, H., Shepherdson, J.C. (eds.). Logic Colloquium’73 (1975)

    Chapter  Google Scholar 

  30. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)

    Google Scholar 

  31. Moltmann, F.: Unbound anaphoric pronouns: E-type, dynamic and atructured-propositions approaches. Synthese 153 (1983)

    Article  MathSciNet  Google Scholar 

  32. Montague, R.: Formal Philosophy. R. Yale University Press, Collected papers edited by Thomason (1974)

    Google Scholar 

  33. Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf’s type theory: an introduction. Oxford University Press (1990)

    Google Scholar 

  34. Ranta, A.: Type-theoretical Grammar. Oxford University Press (1994)

    Google Scholar 

  35. 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)

    Google Scholar 

  36. Sundholm, G.: Proof theory and meaning. Gabbay, D., Guenthner, F. (eds.). Handbook of Philosophical Logic, vol. III (1986)

    Google Scholar 

  37. Sundholm, G.: Constructive generalized quantifiers. Synthese 79(1), 1–12 (1989)

    Article  MathSciNet  Google Scholar 

  38. Tanaka, R.: Generalized quantifiers in dependent type semantics. Talk given at Ohio State University (2015)

    Google Scholar 

  39. The Coq Development Team: The Coq Proof Assistant Reference Manual (Version 8.0), INRIA (2004)

    Google Scholar 

  40. The Univalent Foundations Program: Homotopy type theory: univalent foundations of mathematics. Technical report, Institute for Advanced Study (2013)

    Google Scholar 

  41. Xue, T., Luo, Z., Chatzikyriakidis, S.: Propositional forms of judgemental interpretations. In: Proceedings of the Workshop on Natural Language and Computer Science, Oxford (2018)

    Google Scholar 

Download references

Acknowledgements

Partially supported by EU COST Action EUTYPES (CA15123, Research Network on Types).

Author information

Authors and Affiliations

  1. Royal Holloway, University of London, London, UK

    Zhaohui Luo

Authors
  1. Zhaohui Luo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhaohui Luo .

Editor information

Editors and Affiliations

  1. Department of Mathematics, Stockholm University, Stockholm, Sweden

    Roussanka Loukanova

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

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

Publish with us

Policies and ethics

Search

Navigation