Epsilon 演算的语义与证明论
逻辑
2022-01-31 v1
摘要
Epsilon 算子是一种项形成算子，用于取代普通谓词逻辑中的量词。由于缺乏表现良好的证明系统，以及缺乏对其理论的易懂阐述，这一被低估的形式主义的应用受到了阻碍。针对 Epsilon 演算原始公理证明系统的一个重要早期结果是第一 Epsilon 定理，文中概述了其证明。本文讨论了该系统本身，包括其相对于可能语义解释的情况，并概述了开发具有良好证明论性质的系统所面临的问题。
引用
@article{arxiv.1610.06289,
title = {Semantics and Proof Theory of the Epsilon Calculus},
author = {Richard Zach},
journal= {arXiv preprint arXiv:1610.06289},
year = {2022}
}
备注
arXiv admin note: substantial text overlap with arXiv:1411.3629