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

DOI10.1007/S001530100124MaRDI QIDQ1407600zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(34)

• From axioms to synthetic inference rules via focusing
• Contraction, infinitary quantifiers, and omega paradoxes
• Intermediate logics admitting a structural hypersequent calculus
• Combinatorial analysis of proofs in projective and affine geometry
• Syntactic Completeness of Proper Display Calculi
• Remarks on Barr's theorem: proofs in geometric theories
• 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
• Analytic rules for mereology
• Meaning in use
• No Speedup for Geometric Theories
• Full cut elimination and interpolation for intuitionistic logic with existence predicate
• The Church-Fitch knowability paradox in the light of structural proof theory
• Proof analysis for Lewis counterfactuals
• Proof analysis in modal logic
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Quantified modal logics: one approach to rule (almost) them all!
• 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
• Reasoning about collectively accepted group beliefs
• Proof analysis in intermediate logics
• In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs
• Constructibility and Geometry
• Subintuitionistic logics and their modal companions: a nested approach
• On the proof theory of infinitary modal logic
• Labeled sequent calculi for modal logics and implicit contractions
• Formalizing Kant's rules. A logic of conditional imperatives and permissives
• Geometrisation of first-order logic

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)