Scholarlink

<p>We introduce a new version of arithmetic in all finite types which extends the usual versions with primitive notions of extensionality and extensional equality. This new hybrid version allows us to formulate a strong form of extensionality, which we call converse extensionality. Inspired by Brouwer’s notion of apartness, we show that converse extensionality can be eliminated in a way which improves on results from our previous work. We also explain how standard proof-theoretic interpretations, like realizability and functional interpretations, can be extended to such hybrid systems, and how that might be relevant to proof-mining.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Apartness and the elimination of strong forms of extensionality

  • 期刊论文

  • 发表日期：

    2025年11月16日

查看全文
  • Benno van den Berg

摘要

We introduce a new version of arithmetic in all finite types which extends the usual versions with primitive notions of extensionality and extensional equality. This new hybrid version allows us to formulate a strong form of extensionality, which we call converse extensionality. Inspired by Brouwer’s notion of apartness, we show that converse extensionality can be eliminated in a way which improves on results from our previous work. We also explain how standard proof-theoretic interpretations, like realizability and functional interpretations, can be extended to such hybrid systems, and how that might be relevant to proof-mining.