关于Barr定理的评注：几何理论中的证明
逻辑
2016-03-11 v1
摘要
通常归于Barr的一个定理得出：(A) 从几何理论经典 L_{\infty\omega} 逻辑推导出的几何蕴涵也具有直觉主义证明。Barr定理是拓扑斯性质的，其证明非构造性。文献中也能发现关于该定理去除推导中选择公理能力的神秘评论。本文研究Barr定理的证明论侧面，也旨在阐明选择公理部分。更具体地，给出了 L_{\infty\omega} 的Hauptsatz（主定理）的构造性证明，并用以得到一个(A)的简单证明，该证明可在构造性集合论和Martin-Löf类型论中形式化。
引用
@article{arxiv.1603.03374,
title = {Remarks on Barr's theorem: Proofs in geometric theories},
author = {Michael Rathjen},
journal= {arXiv preprint arXiv:1603.03374},
year = {2016}
}