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

DOI10.1007/s001530100124zbMath1025.03055OpenAlexW2041585656MaRDI QIDQ1407600

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

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

Related Items

From axioms to synthetic inference rules via focusing, Glivenko sequent classes in the light of structural proof theory, Analytic rules for mereology, Syntactic Completeness of Proper Display Calculi, Labeled sequent calculus for justification logics, Contraction, infinitary quantifiers, and omega paradoxes, Labeled sequent calculi for modal logics and implicit contractions, Interpolation in extensions of first-order logic, Intermediate logics admitting a structural hypersequent calculus, Glivenko sequent classes and constructive cut elimination in geometric logics, Formalizing Kant's rules. A logic of conditional imperatives and permissives, Negation-free and contradiction-free proof of the Steiner-Lehmus theorem, Combinatorial analysis of proofs in projective and affine geometry, The Church-Fitch knowability paradox in the light of structural proof theory, Reasoning about collectively accepted group beliefs, Proof analysis in intermediate logics, Proofs and countermodels in non-classical logics, In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs, GEOMETRISATION OF FIRST-ORDER LOGIC, From mathematical axioms to mathematical rules of proof: recent developments in proof analysis, PROOF ANALYSIS FOR LEWIS COUNTERFACTUALS, Meaning in Use, Constructibility and Geometry, Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate, A FORMAL SYSTEM FOR EUCLID’SELEMENTS, On the proof theory of infinitary modal logic, Geometric Rules in Infinitary Logic, Proof analysis in modal logic