是否存在希尔伯特式的纯类型系统？
Are there Hilbert-style Pure Type Systems?
摘要：
对于许多自然演绎风格的逻辑，有一个希尔伯特风格的逻辑与它等价，因为它具有相同的定理（即空上下文的有效判断）。对于直觉主义逻辑，等价的希尔伯特式逻辑的公理可以是命题，它们也被称为组合子I、K和S的类型。希尔伯特风格版本的推理组合逻辑具有公理的公式，这些公理是I，K和S的实际类型语句。由于纯类型系统（PTS）在某种意义上等价于推理组合逻辑系统，因此可以认为希尔伯特式PTS（HPTS）可以以类似的方式为基础。本文证明了一些PTS有非常平凡的等价HPTS，只有公理作为定理，对许多PTS没有等价的HPTS可以存在。最常用的PTS属于这两类。然而，对于一些PTS，包括lambda* 和基于证明助手Coq的PTS，存在非平凡等价的HPTS，其公理是I、K和S的类型语句。
英文摘要：
For many a natural deduction style logic there is a Hilbert-style logic that is equivalent to it in that it has the same theorems (i.e. valid judgements with empty contexts). For intuitionistic logic, the axioms of the equivalent Hilbert-style logic can be propositions which are also known as the types of the combinators I, K and S. Hilbert-style versions of illative combinatory logic have formulations with axioms that are actual type statements for I, K and S. As pure type systems (PTSs)are, in a sense, equivalent to systems of illative combinatory logic, it might be thought that Hilbert-style PTSs (HPTSs) could be based in a similar way. This paper shows that some PTSs have very trivial equivalent HPTSs, with only the axioms as theorems and that for many PTSs no equivalent HPTS can exist. Most commonly used PTSs belong to these two classes. For some PTSs however, including lambda* and the PTS at the basis of the proof assistant Coq, there is a nontrivial equivalent HPTS, with axioms that are type statements for I, K and S.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
