Remarks on Barr’s Theorem: Proofs in Geometric Theories

DOI10.1515/9781501502620-019zbMath1433.03165arXiv1603.03374OpenAlexW2294984609MaRDI QIDQ5221863

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

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

Related Items

Glivenko sequent classes and constructive cut elimination in geometric logics, The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions, Théories géométriques pour l’algèbre des nombres réels, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), On Relating Theories: Proof-Theoretical Reduction, Geometric Rules in Infinitary Logic