首页    期刊浏览 2024年11月05日 星期二
登录注册

文章基本信息

  • 标题:Non-Constructivity in Kan Simplicial Sets
  • 本地全文:下载
  • 作者:Marc Bezem ; Thierry Coquand ; Erik Parmann
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:38
  • 页码:92-106
  • DOI:10.4230/LIPIcs.TLCA.2015.92
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We give an analysis of the non-constructivity of the following basic result: if X and Y are simplicial sets and Y has the Kan extension property, then Y^X also has the Kan extension property. By means of Kripke countermodels we show that even simple consequences of this basic result, such as edge reversal and edge composition, are not constructively provable. We also show that our unprovability argument will have to be refined if one strengthens the usual formulation of the Kan extension property to one with explicit horn-filler operations.
  • 关键词:Constructive logic; simplicial sets; semantics of simple types
国家哲学社会科学文献中心版权所有