Glivenko sequent classes and constructive cut elimination in geometric logics

DOI10.1007/s00153-022-00857-zMaRDI QIDQ6103506

Sara Negri, Eugenio Orlandelli, Giulio Fellin

Publication date: 5 June 2023

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

zbMATH Keywords

infinitary logicconservativitygeometric theoriesconstructive cut eliminationGlivenko sequent classes

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Theories (e.g., algebraic theories), structure, and semantics (18C10) Embedding theorems, universal categories (18B15) Subsystems of classical logic (including intuitionistic logic) (03B20)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Glivenko sequent classes in the light of structural proof theory
• Eliminability of cut in hypersequent calculi for some modal logics of linear frames
• Proof theory. 2nd ed
• Toposes without points
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• Correspondences between classical, intuitionistic and uniform provability
• Minimal from classical proofs
• Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions
• Proof theory for fuzzy logics
• FROM STENIUS’ CONSISTENCY PROOF TO SCHÜTTE’S CUT ELIMINATION FOR ω-ARITHMETIC
• Proof Analysis
• Cut Elimination in the Presence of Axioms
• Geometric Rules in Infinitary Logic
• A NOTE ON THE SEQUENT CALCULI
• Remarks on Barr’s Theorem: Proofs in Geometric Theories
• An interpolation theorem for denumerably long formulas
• Aspects of topoi