Elamur Research⌕
☰
home / papers / 2017 / Factivity and presupposition in Dependent Type Semantics

Factivity and presupposition in Dependent Type Semantics

Paper · 2017 · Ribeka Tanaka, Koji Mineshima and Daisuke Bekki

Summary

The paper asks how a proof-theoretic semantics can explain the inferences that factive verbs such as know license. Previous treatments were mostly model-theoretic. Work in epistemic logic studied knowledge itself but not how language expresses it or what it presupposes. The authors build on Dependent Type Semantics (DTS), which pairs CCG syntax with dependent type theory and represents anaphora with underspecified terms. They extend DTS so that proof objects can be passed around like ordinary arguments. A factive verb can then require evidence that its complement holds. This yields a compositional account of both entailment and presupposition for know. It also gives a formal version of the old distinction between facts and propositions, which explains why factive and non-factive verbs behave differently. The paper is purely theoretical: there are no corpora, models or evaluation numbers. Its value is a precise, computable account that ties anaphora, presupposition and factivity together in one framework.

Key points

  • Written by Ribeka Tanaka, Koji Mineshima and Daisuke Bekki (Ochanomizu University; CREST, JST), the article appeared in 2017 in the Journal of Language Modelling, volume 5, issue 2, on pages 385–420.
  • DTS (Bekki 2014) works in three steps:
    • CCG (Steedman 2000) maps a sentence deterministically to an underspecified representation.
    • Anaphora and presupposition resolution is then cast as type checking.
  • Σ-types act as dynamic existentials, and Π-types act as universals. Projection functions on proof terms carry discourse referents forward, as in the donkey sentence.
  • Common nouns are treated as predicates of type entity → type, not as types (contra Ranta, Luo). The authors argue this explains three things:
    • Predicate nominals ("John is a man") introduce no referent.
    • Pronouns pointing back to such nominals surface as it or which.
    • An equality-based analysis would wrongly make negated and conditional sentences presuppose the predication.
  • Factivity is modelled through proof objects as first-class terms. This gives a type-level split between facts and propositions.

Interesting ideas

  • I1. A factive verb takes the clause together with a witness that the clause is true, while a non-factive verb takes only the clause; the difference sits in the verb's argument type rather than in an ad hoc rule.
  • I2. Resolving a pronoun or presupposition is framed as finding a context term with the required type, so the resolver has a checkable success criterion and leaves an explicit trace.
  • I3. Interpretation is split into a deterministic mapping to an underspecified form plus a separate resolution step, which keeps syntax-driven composition clean and isolates context-dependent choices.
  • I4. Common nouns are treated as predicates, so a predicative sentence adds a property to an existing individual instead of creating a new one, matching the fact that such nominals cannot be referred back to with he/she.
  • I5. Embedding a sentence under negation or a conditional is used as a diagnostic: content that still follows is presupposed, not merely entailed.

For Mova

How these ideas could serve Mova, our small open language model — its files, stages and tests:

  • I1 (world): for "X knows that P", add P to the shared world with X's knowledge as provenance, while for "X believes that P", keep P only inside X's belief space.
  • I2 (frames): coreference could search the world for entities that satisfy the slot's type constraint and log that constraint as the explanation for each link.
  • I3 (frames): build frames from the UD tree with explicit open placeholders for pronouns and presupposed content, then fill them in a dedicated, auditable pass.
  • I4 (world): copular "is a N" should attach a class or property to the subject entity and must not spawn a new entity that later pronouns could grab.
  • I5 (learn): auto-generate negated and "if…" variants of test items as negative controls to check that the system keeps presupposed facts but drops plain entailments.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Ochanomizu UniversityTokyo · Japan2 works · 67 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 works

🧭 Topics 1Research subjects and languages the work is about.Implicature · 138 works

Cite

Cite as Ribeka Tanaka, Koji Mineshima and Daisuke Bekki. 2017. Factivity and presupposition in Dependent Type Semantics. Journal of Language Modelling.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.15398/jlm.v5i2.153

@article{tanaka2017factivity,
  title = {{Factivity and presupposition in Dependent Type Semantics}},
  author = {Ribeka Tanaka, Koji Mineshima and Daisuke Bekki},
  journal = {Journal of Language Modelling},
  year = {2017},
  doi = {10.15398/jlm.v5i2.153},
  url = {https://doi.org/10.15398/jlm.v5i2.153}
}

References

52 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Nicholas Asher (2011), Lexical Meaning in Context: A Web of Words, Cambridge University Press, Cambridge. find
  2. Nicholas Asher and Zhaohui Luo (2012), Formalisation of coercions in lexical semantics, in E. Chemla, V. Homer, and G. Winterstein, editors, Proceedings of Sinn und Bedeutung 17, pp. 63–80, Paris, http://semanticsarchive.net/sub2012/ . ↗
  3. David I. Beaver (2001), Presupposition and Assertion in Dynamic Semantics, CSLI Publications, Stanford. find
  4. Daisuke Bekki (2014), Representing anaphora with dependent types, in N. Asher and S. Soloviev, editors, Logical Aspects of Computational Linguistics: 8th International Conference, LACL 2014, Proceedings, volume 8535 of Lecture Notes in Computer Science, pp. 14–29, Springer, Heidelberg. find
  5. Daisuke Bekki and Nicholas Asher (2013), Logical polysemy and subtyping, in Y. Motomura, A. Butler, and D. Bekki, editors, New Frontiers in Artificial Intelligence: JSAI-isAI 2012 Workshops, Revised Selected Papers, volume 7856 of Lecture Notes in Computer Science, pp. 17–24, Springer, Heidelberg. find
  6. Daisuke Bekki and Koji Mineshima (2017), Context-passing and underspecification in Dependent Type Semantics, in S. Chatzikyriakidis and Z. Luo, editors, Modern Perspectives in Type-Theoretical Semantics, volume 98 of Studies in Linguistics and Philosophy, pp. 11–41, Springer, Heidelberg. find
  7. Daisuke Bekki and Miho Satoh (2015), Calculating projections via type checking, in R. Cooper and C. Retoré, editors, ESSLLI proceedings of the TYTLES workshop on Type Theory and Lexical Semantics ESSLLI2015, Barcelona. find
  8. Stergios Chatzikyriakidis and Zhaohui Luo (2014), Natural language inference in Coq, Journal of Logic, Language and Information, 23(4):441–480. find
  9. Robin Cooper (1983), Quantification and Syntactic Theory, Reidel, Dordrecht. ↗
  10. Rogelio Dávila-Pérez (1995), Semantics and Parsing in Intuitionistic Categorial Grammar, Ph.D. thesis, University of Essex. find
  11. Paul Egré (2008), Question-embedding and factivity, Grazer Philosophische Studien, 77(1):85–125. ↗
  12. Delia Graff Fara (2001), Descriptions as predicates, Philosophical Studies, 102:1–42, originally published under the name “Delia Graff”. find
  13. Chris Fox and Shalom Lappin (2005), Foundations of Intensional Semantics, Blackwell, Oxford. find
  14. Jonathan Ginzburg (1995a), Resolving questions, I, Linguistics and Philosophy, 18(5):459–527. find
  15. Jonathan Ginzburg (1995b), Resolving questions, II, Linguistics and Philosophy, 18(6):567–609. find
  16. Jeroen Groenendijk and Martin Stokhof (1991), Dynamic predicate logic, Linguistics and Philosophy, 14(1):39–100. find
  17. Irene Heim (1982), The Semantics of Definite and Indefinite Noun Phrases, Ph.D. thesis, University of Massachusetts, Amherst. find
  18. Irene Heim (1983), On the projection problem for presuppositions, in M. Barlow, D. Flickinger, and M. Wescoat, editors, Proceedings of the Second West Coast Conference on Formal Linguistics, pp. 114–125, Stanford University Press, Stanford, CA. find
  19. Jaakko Hintikka (1962), Knowledge and Belief: An Introduction to the Logic of the Two Notions, Cornell University Press, Ithaca, NY. find
  20. Jaakko Hintikka (1969), Semantics for propositional attitudes, in J. W. Davis, D. J. Hockney, and W. K. Wilson, editors, Philosophical Logic, volume 20 of Synthese Library, pp. 21–45, Reidel, Dordrecht. find
  21. William Alvin Howard (1980), The formulae-as-types notion of construction, in J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 480–490, Academic Press, London. find
  22. Hans Kamp, Josef van Genabith, and Uwe Reyle (2011), Discourse Representation Theory, in D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 15, pp. 125–394, Springer, Heidelberg. find
  23. Lauri Karttunen (1971), Implicative verbs, Language, 47(2):340–358. find
  24. Lauri Karttunen and Stanley Peters (1979), Conventional implicatures, in C. K. Oh and D. A. Dinneen, editors, Syntax and Semantics 11: Presupposition, pp. 1–56, Academic Press, New York, NY. find
  25. Jeffrey C. King (2002), Designating propositions, The Philosophical Review, 111(3):341–371. find
  26. Eriko Kinoshita, Koji Mineshima, and Daisuke Bekki (2016), An analysis of selectional restrictions with Dependent Type Semantics, in Proceedings of the 13th International Workshop on Logic and Engineering of Natural Language Semantics (LENLS13), pp. 100–113, Kanagawa. find
  27. Paul Kiparsky and Carol Kiparsky (1970), Fact, in M. Bierwisch and K. E. Heidolph, editors, Progress in Linguistics, pp. 143–173, de Gruyter Mouton, Berlin. find
  28. Emiel Krahmer and Paul Piwek (1999), Presupposition projection as proof construction, in H. Bunt and R. Muskens, editors, Computing Meaning: Volume 1, volume 73 of Studies in Linguistics and Philosophy, pp. 281–300, Kluwer Academic Publishers, Dordrecht. find
  29. Yusuke Kubota and Robert Levine (2017), Scope parallelism in coordination in Dependent Type Semantics, in M. Otake, S. Kurahashi, Y. Ota, K. Satoh, and D. Bekki, editors, New Frontiers in Artificial Intelligence: JSAI-isAI 2015 Workshops, Revised Selected Papers, volume 10091 of Lecture Notes in Artificial Intelligence, pp. 149–162, Springer, Heidelberg. find
  30. Susumu Kuno (1970), Some properties of non-referential noun phrases, in R. Jakobson and S. Kawamoto, editors, Studies in General and Oriental Linguistics. Presented to S. Hattori on Occasion of his Sixtieth Birthday, pp. 348–373, TEC, Tokyo. find
  31. Zhaohui Luo (2012a), Common nouns as types, in D. Béchet and A. Dikovsky, editors, Logical Aspects of Computational Linguistics: 7th International Conference, LACL 2012, Proceedings, volume 7351 of Theoretical Computer Science and General Issues, pp. 173–185, Springer, Heidelberg. find
  32. Zhaohui Luo (2012b), Formal semantics in modern type theories with coercive subtyping, Linguistics and Philosophy, 35(6):491–513. find
  33. Per Martin-Löf (1984), Intuitionistic Type Theory. Notes by G. Sambin, Bibliopolis, Naples. find
  34. John-Jules Ch Meyer and Wiebe van der Hoek (2004), Epistemic Logic for AI and Computer Science, Cambridge University Press, Cambridge. find
  35. Line Mikkelsen (2005), Copular Clauses: Specification, Predication and Equation, John Benjamins, Amsterdam. find
  36. Line Mikkelsen (2011), Copular clauses, in C. Maienborn, K. von Heusinger, and P. Portner, editors, Semantics: An International Handbook of Natural Language Meaning, volume 2, pp. 1805–1829, de Gruyter Mouton, Berlin. find
  37. Richard Montague (1973), The proper treatment of quantification in ordinary English, in P. Suppes, J. Moravcsik, and J. Hintikka, editors, Approaches to Natural Language, pp. 221–242, Kluwer Academic Publishers, Dordrecht. find
  38. Bengt Nordström, Kent Petersson, and Jan M. Smith (1990), Programming in Martin-Löf’s Type Theory: An Introduction, Oxford University Press, Oxford. find
  39. Terence Parsons (1993), On denoting propositions and facts, Philosophical Perspectives, 7:441–460. find
  40. Paul Piwek and Emiel Krahmer (2000), Presuppositions in context: constructing bridges, in P. Bonzon, M. Cavalcanti, and R. Nossum, editors, Formal Aspects of Context, volume 20 of Applied Logic Series, pp. 85–106, Kluwer Academic Publishers, Dordrecht. find
  41. Aarne Ranta (1994), Type-Theoretical Grammar, Oxford University Press, Oxford. find
  42. Christian Retoré (2014), The Montagovian generative lexicon ΛT y n : a type theoretical framework for natural language semantics, in R. Matthes and A. Schubert, editors, 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics, pp. 202–229, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, http://drops.dagstuhl.de/opus/volltexte/2014/4633/ . ↗
  43. Bertrand Russell (1919), Introduction to Mathematical Philosophy, George Allen & Unwin, London. find
  44. Mark Steedman (2000), The Syntactic Process, MIT Press, Cambridge, MA. ↗
  45. Göran Sundholm (1986), Proof Theory and Meaning, in D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 3, pp. 471–506, Reidel, Dordrecht. find
  46. Göran Sundholm (1989), Constructive generalized quantifiers, Synthese, 79(1):1–12. find
  47. Ribeka Tanaka (2014), A proof-theoretic approach to generalized quantifiers in dependent type semantics, in R. de Haan, editor, Proceedings of the ESSLLI2014 Student Session, pp. 140–151, Tübingen, http://www.kr.tuwien.ac.at/drm/dehaan/stus2014/proceedings.pdf . ↗
  48. Ribeka Tanaka, Koji Mineshima, and Daisuke Bekki (2015), Resolving modal anaphora in Dependent Type Semantics, in T. Murata, K. Mineshima, and D. Bekki, editors, New Frontiers in Artificial Intelligence: JSAI-isAI 2014 Workshops, Revised Selected Papers, pp. 83–98, Springer, Heidelberg. find
  49. Ribeka Tanaka, Yuki Nakano, and Daisuke Bekki (2014), Constructive generalized quantifiers revisited, in Y. Nakano, K. Satoh, and D. Bekki, editors, New Frontiers in Artificial Intelligence: JSAI-isAI 2013 Workshops, Revised Selected Papers, volume 8417 of Lecture Notes in Computer Science, pp. 115–124, Springer, Heidelberg. find
  50. Wataru Uegaki (2016), Content nouns and the semantics of question-embedding, Journal of Semantics, 33(4):623–660. find
  51. Rob A. van der Sandt (1992), Presupposition projection as anaphora resolution, Journal of Semantics, 9:333–377. find
  52. Zeno Vendler (1972), Res Cogitans: An Essay in Rational Psychology, Cornell University Press, Ithaca, NY. This work is licensed under the Creative Commons Attribution 3.0 Unported License. http://creativecommons.org/licenses/by/3.0/ ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/tanaka-2017-factivity-presupposition-dependent-type-semantics/