Remarks on Barr's theorem: Proofs in geometric theories
英文摘要：
A theorem, usually attributed to Barr, yields that (A) geometric implications deduced in classical L_{\inftyω} logic from geometric theories also have intuitionistic proofs. Barr's theorem is of a topos-theoretic nature and its proof is non-constructive. In the literature one also finds mysterious comments about the capacity of this theorem to remove the axiom of choice from derivations. This article investigates the proof-theoretic side of Barr's theorem and also aims to shed some light on the axiom of choice part. More concretely, a constructive proof of the Hauptsatz for L_{\inftyω} is given and is put to use to arrive at a simple proof of (A) that is formalizable in constructive set theory and Martin-Loef type theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
