作为逻辑丰富的类型论的Weyl预言经典数学
Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory
摘要：
我们构建了一个逻辑丰富的类型论LTTW，它与赫尔曼·外尔在《连续论》中提出的基础的谓词系统密切对应。我们正式许多结果从这本书在LTTW，包括外尔的定义的基数的一套和几个结果从真正的分析，使用证明助手塑料，实现了逻辑框架LF。这个案例研究显示了如何类型论可以用来表示一个非建设性的数学基础。
英文摘要：
We construct a logic-enriched type theory LTTW that corresponds closely to the predicative system of foundations presented by Hermann Weyl in Das Kontinuum. We formalise many results from that book in LTTW, including Weyl's definition of the cardinality of a set and several results from real analysis, using the proof assistant Plastic that implements the logical framework LF. This case study shows how type theory can be used to represent a non-constructive foundation for mathematics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
