Remarks on Barr's theorem: Proofs in geometric theories

TL;DR

This paper provides a constructive proof of Barr's theorem for geometric theories, clarifying its proof-theoretic aspects and its relation to the axiom of choice, with implications for formalizable logic systems.

Contribution

It offers the first constructive proof of Barr's theorem and explores its implications for removing the axiom of choice in geometric logic.

Findings

Constructive proof of the Hauptsatz for L_{ olineomega}

Simplified proof of Barr's theorem formalizable in constructive set theory

Clarification of the theorem's relation to the axiom of choice

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.