Cut Elimination in the Presence of Axioms

DOI10.2307/420956MaRDI QIDQ4254567zbMATH OpenOpenAlexWikidataFDO

Authors Sara Negri, Jan von Plato

Publication date 6 April 2000

Published in The Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/9fb30639095e2197a4ed3be6e8f663bf49ad3862, http://www.math.ucla.edu/~asl/bsl/0404-toc.htm

zbMATH Keywords

sequent calculuscut-eliminationnon-logical inference rule

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Recommendations

• The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality
• Cut elimination for Gentzen's sequent calculus with equality and logic of partial terms
• Cut Elimination In Situ
• Cut Elimination in ε‐Calculi

Cited in

(76)

• Cut-Simulation and Impredicativity
• Syntax for semantics: Krull's maximal ideal theorem
• Incomplete symbols -- definite descriptions revisited
• From axioms to synthetic inference rules via focusing
• Contraction, infinitary quantifiers, and omega paradoxes
• Towards formal Baer criteria
• Cut elimination for Gentzen's sequent calculus with equality and logic of partial terms
• Uniqueness of axiomatic extensions of cut-free classical propositional logic
• A more unified approach to free logics
• Consistency of Heyting arithmetic in natural deduction
• Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs
• Cut-elimination for simple type theory with an axiom of choice
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Proof-theoretic analysis of the logics of agency: the deliberative STIT
• Syntactic forcing models for coherent logic
• On the metainferential solution to the semantic paradoxes
• scientific article; zbMATH DE number 1471986 (Why is no real title available?)
• Combinatorial analysis of proofs in projective and affine geometry
• Syntactic Completeness of Proper Display Calculi
• Axiom Directed Focusing
• Glivenko sequent classes and constructive cut elimination in geometric logics
• A first-order expansion of Artemov and Protopopescu's intuitionistic epistemic logic
• A universal algorithm for Krull's theorem
• Cut-Elimination for SBL
• An investigation into intuitionistic logic with identity
• Geometric Rules in Infinitary Logic
• scientific article; zbMATH DE number 6680140 (Why is no real title available?)
• Analytic rules for mereology
• Meaning in use
• Is, ought, and cut
• Towards a clausal analysis of cut-elimination
• Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
• Tautology elimination, cut elimination, and S5
• Corrected upper bounds for free-cut elimination
• The Church-Fitch knowability paradox in the light of structural proof theory
• Proof analysis for Lewis counterfactuals
• Cut-Simulation in Impredicative Logics
• Axiomatizing geometric constructions
• Proof analysis in modal logic
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Forms of the Pasch axiom in ordered geometry
• Negation-free and contradiction-free proof of the Steiner-Lehmus theorem
• Algebra, proof theory and applications for a logic of propositions, actions and adjoint modal operators
• A two-dimensional metric temporal logic
• Sequent calculi for \(\mathsf{SCI}\)
• Focusing Gentzen's LK proof system
• Logic and majority voting
• Point-Free Spectra of Linear Spreads
• Cut elimination for a calculus with context-dependent rules
• Labeled sequent calculus for justification logics
• Proofs and countermodels in non-classical logics
• Interpolation in extensions of first-order logic
• Method of invariant transformations and logical deduction
• Faithfulness for naive validity
• THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
• Reasoning about collectively accepted group beliefs
• Proof analysis in intermediate logics
• The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions
• On Constructive Cut Admissibility in Deduction Modulo
• Naive set theory and nontransitive logic
• Towards a semantic characterization of cut-elimination
• From Stenius' consistency proof to Schütte's cut elimination for \(\omega\)-arithmetic
• On the elimination of quantifier-free cuts
• The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality
• Lemma and cut strategies for propositional model elimination
• The intensional side of algebraic-topological representation theorems
• Proof Theory for Distributed Knowledge
• PRIORITY MERGE AND INTERSECTION MODALITIES
• Cut elimination for entailment relations
• A Semantic Proof that Reducibility Candidates entail Cut Elimination
• Herzberger's limit rule with labelled sequent calculus
• Neutral free logic: motivation, proof theory and models
• Absorbing the structural rules in the sequent calculus with additional atomic rules
• scientific article; zbMATH DE number 2247256 (Why is no real title available?)
• A NOTE ON THE SEQUENT CALCULI
• Unwinding a Non-effective Cut Elimination Proof

This page was built for publication: Cut Elimination in the Presence of Axioms

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