作为逻辑增强类型理论的Weyl的谓词经典数学
计算机科学中的逻辑
2009-12-26 v3
摘要
我们构建了一个逻辑增强类型理论LTTW，它与Hermann Weyl在《连续统》中提出的谓词性基础系统密切相关。我们使用实现逻辑框架LF的证明助手Plastic，在LTTW中形式化了该书中的许多结果，包括Weyl对集合基数的定义以及实分析中的若干结果。这个案例研究展示了如何使用类型理论来表示非构造性的数学基础。
引用
@article{arxiv.0809.2061,
title = {Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory},
author = {Robin Adams and Zhaohui Luo},
journal= {arXiv preprint arXiv:0809.2061},
year = {2009}
}
备注
31 pages, 6 figures. Accepted for publication in ACM TOCL. v2: Corrected a broken citation in v1. v3: Final version, revised after referees' comments