E-HA$^w$ 在 HA$^w$ 中的一种解释

Félix Castro

doi:10.4204/EPTCS.396.5

E-HA$^w$ 在 HA$^w$ 中的一种解释

计算机科学中的逻辑 2023-11-20 v1

作者: Félix Castro

在 arXiv 上查看 ↗ PDF ↗ DOI ↗

摘要

高阶算术（HA $^w$ ）是一阶多类理论。它是海廷算术的保守扩张，通过将项的语法扩展到整个 System T 得到：此处关注的对象是高阶泛函。虽然自然数之间的相等由皮亚诺公理规定，但泛函之间的相等如何定义？由此问题产生了 HA $^w$ 的不同版本，例如外延版本（E-HA $^w$ ）和内涵版本（I-HA $^w$ ）。在本文中，我们将看到对偏等价关系的研究如何引导我们设计一种从 E-HA $^w$ 到 HA $^w$ 的由参数性驱动的翻译。

关键词

高阶算术外延版本内涵版本偏等价关系参数性翻译 System T

引用

@article{arxiv.2311.10578,
  title  = {An Interpretation of E-HA$^w$ inside HA$^w$},
  author = {Félix Castro},
  journal= {arXiv preprint arXiv:2311.10578},
  year   = {2023}
}

备注

In Proceedings LFMTP 2023, arXiv:2311.09918

E-HA$^w$ 在 HA$^w$ 中的一种解释

摘要

关键词

引用

备注

相关论文