Cut elimination, identity elimination, and interpolation in super-Belnap logics
From MaRDI portal
(Redirected from Publication:1685571)
Abstract: We develop a Gentzen-style proof theory for super-Belnap logics (extensions of the four-valued Dunn-Belnap logic), expanding on an approach initiated by Pynko. We show that just like substructural logics may be understood proof-theoretically as logics which relax the structural rules of classical logic but keep its logical rules as well as the rules of Identity and Cut, super-Belnap logics may be seen as logics which relax Identity and Cut but keep the logical rules as well as the structural rules of classical logic. A generalization of the cut elimination theorem for classical propositional logic is then proved and used to establish interpolation for various super-Belnap logics. In particular, we obtain an alternative syntactic proof of a refinement of the Craig interpolation theorem for classical propositional logic discovered recently by Milne.
Recommendations
- An algebraic view of super-Belnap logics
- An infinity of super-Belnap logics
- Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics
- Cut-free single-succedent systems revisited
- Interpolation for intermediate logics via hyper- and linear nested sequents
Cites work
- scientific article; zbMATH DE number 3648682 (Why is no real title available?)
- scientific article; zbMATH DE number 4033738 (Why is no real title available?)
- scientific article; zbMATH DE number 3504935 (Why is no real title available?)
- scientific article; zbMATH DE number 1497485 (Why is no real title available?)
- scientific article; zbMATH DE number 945663 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- A non-classical refinement of the interpolation property for classical propositional logic
- A unified semantic framework for fully structural propositional sequent systems
- About some symmetries of negation
- Abstract algebraic logic. An introductory textbook
- An algebraic view of super-Belnap logics
- An infinity of super-Belnap logics
- Belnap's Four-Valued Logic and De Morgan Lattices
- Canonical Calculi: Invertibility, Axiom Expansion and (Non)-determinism
- Characterizing Belnap's Logic via De Morgan's Laws
- Correspondences between gentzen and hilbert systems
- Gentzen's cut-free calculus versus the logic of paradox
- How a Computer Should Think
- Interpolation and three-valued logics
- Intuitive semantics for first-degree entailments and `coupled trees'
- Nothing but the truth
- Order algebraizable logics
- Subprevarieties versus extensions. Application to the logic of paradox
- Syntactical and semantical properties of simple type theory
- THE LATTICE OF SUPER-BELNAP LOGICS
- The logic of paradox
- Which structural rules admit cut elimination? An algebraic criterion
Cited in
(9)- Inferences and metainferences in \(\mathsf{ST}\)
- Cut-elimination and interpolation for \(\Omega\)-logic
- An algebraic view of super-Belnap logics
- Sequent-calculi for metainferential logics
- Editorial introduction
- Sequent calculi for first-order ST
- K3, Ł3, LP, RM3, A3, FDE, M: how to make many-valued logics work for you
- \(\mathsf{ST}\) and \(\mathsf{TS}\) as product and sum
- The value of the one value: \textit{exactly true logic} revisited
This page was built for publication: Cut elimination, identity elimination, and interpolation in super-Belnap logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1685571)
