论证明无关类型理论的强度
计算机科学中的逻辑
2015-07-01 v2
摘要
我们提出了一种类型理论，其中将某种证明无关性内建到转换规则中。我们认为，当类型理论被用作定理证明器背后的逻辑形式体系时，这一特性非常有用。我们还展示了其与PVS理论中子集类型的密切关系。我们证明，在这些理论中，由于额外的外延性，选择公理蕴含了相等性的可判定性，即近乎经典逻辑。最后，我们描述了一个简单的集合论语义。
引用
@article{arxiv.0808.3928,
title = {On the strength of proof-irrelevant type theories},
author = {Benjamin Werner},
journal= {arXiv preprint arXiv:0808.3928},
year = {2015}
}
备注
20 pages, Logical Methods in Computer Science, Long version of IJCAR 2006 paper