Syntactic forcing models for coherent logic

DOI10.1016/j.indag.2018.06.004zbMath1437.03188arXiv1712.07743OpenAlexW2963122775MaRDI QIDQ1788327

Marc Bezem, Ulrik Buchholtz, Thierry Coquand

Publication date: 8 October 2018

Published in: Indagationes Mathematicae. New Series (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Open maps of toposes
• Exact completions and small sheaves
• Cut Elimination in the Presence of Axioms
• Constructive Sheaf Semantics
• Proof analysis beyond geometric theories: from rule systems to systems of rules
• On the rules of proof in the pure functional calculus of the first order