Remarks on Barr's theorem: Proofs in geometric theories
Logic
2016-03-11 v1
Abstract
A theorem, usually attributed to Barr, yields that (A) geometric implications deduced in classical L_{\infty\omega} 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\omega} 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.
Keywords
Cite
@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}
}