Contraction-free sequent calculi for geometric theories with an application to Barr's theorem

DOI10.1007/S001530100124zbMATH Open1025.03055OpenAlexW2041585656MaRDI QIDQ1407600FDOQ1407600

Authors: Sara Negri 

Publication date: 16 September 2003

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

Full work available at URL: https://doi.org/10.1007/s001530100124

Recommendations

• Remarks on Barr's theorem: proofs in geometric theories
• scientific article; zbMATH DE number 7166981
• Admissibility of structural rules for extensions of contraction-free sequent calculi
• Proof analysis beyond geometric theories: from rule systems to systems of rules
• scientific article; zbMATH DE number 1795222

zbMATH Keywords

cut eliminationreal closed fieldRobinson arithmeticgeometric theoriesBarr's theoremgeometric implication

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Categorical logic, topoi (03G30) Topoi (18B25)

Cited In (34)

• From axioms to synthetic inference rules via focusing
• Contraction, infinitary quantifiers, and omega paradoxes
• Intermediate logics admitting a structural hypersequent calculus
• Syntactic Completeness of Proper Display Calculi
• Remarks on Barr's theorem: proofs in geometric theories
• Combinatorial analysis of proofs in projective and affine geometry
• Glivenko sequent classes and constructive cut elimination in geometric logics
• Glivenko sequent classes in the light of structural proof theory
• Geometric Rules in Infinitary Logic
• Proof analysis beyond geometric theories: from rule systems to systems of rules
• Meaning in use
• No Speedup for Geometric Theories
• Full cut elimination and interpolation for intuitionistic logic with existence predicate
• Analytic rules for mereology
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• The Church-Fitch knowability paradox in the light of structural proof theory
• Proof analysis for Lewis counterfactuals
• Quantified modal logics: one approach to rule (almost) them all!
• Proof analysis in modal logic
• Negation-free and contradiction-free proof of the Steiner-Lehmus theorem
• A general Glivenko-Gödel theorem for nuclei
• From mathematical axioms to mathematical rules of proof: recent developments in proof analysis
• Labeled sequent calculus for justification logics
• Proofs and countermodels in non-classical logics
• Interpolation in extensions of first-order logic
• In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs
• Reasoning about collectively accepted group beliefs
• Proof analysis in intermediate logics
• Subintuitionistic logics and their modal companions: a nested approach
• Constructibility and Geometry
• On the proof theory of infinitary modal logic
• Formalizing Kant's rules. A logic of conditional imperatives and permissives
• Geometrisation of first-order logic
• Labeled sequent calculi for modal logics and implicit contractions

This page was built for publication: Contraction-free sequent calculi for geometric theories with an application to Barr's theorem

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