是否存在希尔伯特风格的纯类型系统？
计算机科学中的逻辑
2015-07-01 v2
摘要
对于许多自然演绎风格的逻辑，都存在一个与之等价的希尔伯特风格逻辑，即它们具有相同的定理（亦即空上下文下的有效判断）。对于直觉主义逻辑，等价希尔伯特风格逻辑的公理是那些也被称为组合子 I、K 和 S 的类型的命题。病态组合逻辑的希尔伯特风格版本具有这样的公式化形式：其公理是 I、K 和 S 的实际类型陈述。由于纯类型系统（PTSs）在某种意义上等价于病态组合逻辑系统，人们可能会认为希尔伯特风格的 PTSs（HPTSs）也可以以类似方式构建。本文表明，某些 PTSs 具有非常平凡的等价 HPTSs，其定理仅包含公理；而对于许多 PTSs，根本不存在等价的 HPTS。大多数常用的 PTSs 属于这两类。然而，对于某些 PTSs，包括 lambda* 和作为证明助手 Coq 基础的 PTS，存在非平凡的等价 HPTS，其公理是 I、K 和 S 的类型陈述。
引用
@article{arxiv.0707.0890,
title = {Are there Hilbert-style Pure Type Systems?},
author = {M. W. Bunder and W. M. J. Dekkers},
journal= {arXiv preprint arXiv:0707.0890},
year = {2015}
}
评论
Accepted in Logical Methods in Computer Science