Remarks on Barr's theorem: proofs in geometric theories

DOI10.1515/9781501502620-019MaRDI QIDQ5221863zbMATH OpenOpenAlexFDO

Authors Michael Rathjen

Publication date 3 April 2020

Published in Concepts of Proof in Mathematics, Philosophy, and Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.03374

zbMATH Keywords

toposaxiom of choicegeometric theorycut elimination in \(\mathcal{L}_{\infty\omega}\)

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Metamathematics of constructive systems (03F50) Categorical logic, topoi (03G30) Topoi (18B25) Other infinitary logic (03C75)

Abstract: A theorem, usually attributed to Barr, yields that (A) geometric implications deduced in classical L_{inftyomega} 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_{inftyomega} 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.

Recommendations

• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• scientific article; zbMATH DE number 2019830
• scientific article; zbMATH DE number 7166981
• Proof analysis beyond geometric theories: from rule systems to systems of rules
• Proof interpretations. Theoretical and practical aspects.

Cited in

(10)

• No Speedup for Geometric Theories
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Geometric Rules in Infinitary Logic
• On Relating Theories: Proof-Theoretical Reduction
• Geometric theories for the algebra of real numbers
• scientific article; zbMATH DE number 1251510 (Why is no real title available?)
• Glivenko sequent classes and constructive cut elimination in geometric logics
• The fundamental theorem of calculus within a geometric context based on Barrow's work
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions

This page was built for publication: Remarks on Barr's theorem: proofs in geometric theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5221863)