Remarks on Barr's theorem: proofs in geometric theories

DOI10.1515/9781501502620-019zbMATH Open1433.03165arXiv1603.03374OpenAlexW2294984609MaRDI QIDQ5221863FDOQ5221863

Authors: Michael Rathjen 

Publication date: 3 April 2020

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

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.

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

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.

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)

Cited In (9)

• Title not available (Why is that?)
• Glivenko sequent classes and constructive cut elimination in geometric logics
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Geometric Rules in Infinitary Logic
• Théories géométriques pour l’algèbre des nombres réels
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• The fundamental theorem of calculus within a geometric context based on Barrow's work
• The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions
• On Relating Theories: Proof-Theoretical Reduction

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)