The proof by cases property and its variants in structural consequence relations
The paper studies the different flavors of the proof by cases property in the setting of (not necessarily finitary) abstract algebraic logic. Let \(\nabla(p, q, \vec{r})\) be a set of formulas in two variables \(p, q\) and possible parameters \(\vec{r}\) and \(\phi \nabla \psi\) denotes \(\bigcup\{\nabla(\phi,\psi,\vec{\alpha}) \;| \;\vec{\alpha} \in Fm^{\leq \omega}\}\). Given sets \(\Phi,\Psi \subseteq Fm\), \(\Phi \nabla \Psi\) denotes the set \(\bigcup\{\{\phi \nabla \psi \;| \;\phi \in \Phi, \psi \in \Psi\}\). A parameterized set \((\nabla,p, q,\vec{r})\) of formulas is a p-protodisjunction (or just protodisjunction if \(\nabla\) has no parameters) in a logic \(L\) whenever (PD) \(\quad \quad \phi \vdash_L \phi \nabla \psi \text{ and } \psi \vdash_L \phi \nabla \psi.\) Let \(L\) be a logic, \(\Gamma\) be a set of formulas and \(\phi,\psi, \chi\) be formulas. Then, the following flavors of the proof by cases property (PCP) can be defined: \(\quad\) PCP: if \(\Gamma, \phi \vdash_L \chi\) and \(\Gamma, \phi \vdash_L \chi\), then \(\Gamma, \phi \nabla \psi \vdash_L \chi\) \(\quad\) wPCP: if \(\phi \vdash_L \chi\) and \(\psi \vdash_L \chi\), then \(\phi \nabla \psi \vdash_L \chi\) \(\quad\) fPCP: if \(\Gamma, \phi \vdash_L \chi\) and \(\Gamma, \phi \vdash_L \chi\), then \(\Gamma, \phi \nabla \psi \vdash_L \chi\) for every finite \(\Gamma\) \(\quad\) sPCP: if \(\Gamma,\Phi \vdash_L \chi\) and \(\Gamma,\Psi \vdash_L \chi\), then \(\Gamma,\Phi\nabla \Psi \vdash_L \chi\). \(\nabla\) is a strong p-disjunction (resp. p-disjunction, resp. weak p-disjunction) if it satisfies the sPCP (resp. PCP, resp. wPCP). If \(\nabla\) has no parameters, the prefix `p-' is dropped. Also, a logic \(L\) is strongly (p-)disjunctional (resp. (p-)disjunctional, resp. weakly (p-)disjunctional) if it has a strong (p-)disjunction (resp. a (p-)disjunction, resp. a weak (p-)disjunction). A logic \(L\) is strongly disjunctive (resp. disjunctive, resp. weakly disjunctive) if it has a strong disjunction (resp. a disjunction, resp. a weak disjunction) given by a single parameter-free formula. It is established that all twelve classes of logics defined above are mutually different and form a 12-element meet lattice. In Section 4, a syntactical characterization of (p)-disjuctional logic is given. Section 5 is dedicated to applications.
- Logics with disjunction and proof by cases
- An algebraic approach to the disjunction property of substructural logics
- Disjunction property and complexity of substructural logics
- Disjunctive and conjunctive multiple-conclusion consequence relations
- A Generalization of Maksimova’s Criterion for the Disjunction Property
- A propositional calculus with denumerable matrix
- A survey of abstract algebraic logic
- Algebraic logic for classical conjunction and disjunction
- Algebraizable logics
- Equational bases for joins of residuated-lattice varieties
- scientific article; zbMATH DE number 3833960 (Why is no real title available?)
- scientific article; zbMATH DE number 3652338 (Why is no real title available?)
- scientific article; zbMATH DE number 67022 (Why is no real title available?)
- scientific article; zbMATH DE number 922613 (Why is no real title available?)
- scientific article; zbMATH DE number 2196609 (Why is no real title available?)
- Implicational (semilinear) logics. I: A new hierarchy
- Leibniz filters and the strong version of a protoalgebraic logic
- Local deductions theorems
- Logics with disjunction and proof by cases
- Matrices, primitive satisfaction and finitely based logics
- Metamathematics of fuzzy logic
- Proof of the independence of the primitive symbols of Heyting's calculus of propositions
- Proper semantics for substructural logics, from a stalker theoretic point of view
- Protoalgebraic logics
- Residuated lattices. An algebraic glimpse at substructural logics
- Selfextensional logics with a conjunction
- THE STRUCTURE OF COMMUTATIVE RESIDUATED LATTICES
- Update to ``A survey of abstract algebraic logic
- An algebraic view of super-Belnap logics
- Eliminating disjunctions by disjunction elimination
- On strong standard completeness in some \(\mathrm{MTL}_\Delta\) expansions
- Selfextensional logics with a distributive nearlattice term
- Implicational (semilinear) logics. III: Completeness properties
- Extension properties and subdirect representation in abstract algebraic logic
- Strong standard completeness for continuous t-norms
- Deductive systems with multiple-conclusion rules and the disjunction property
- A new hierarchy of infinitary logics in abstract algebraic logic
- Implicational (semilinear) logics. II: Additional connectives and characterizations of semilinearity
- Hypersequent rules with restricted contexts for propositional modal logics
- A study of truth predicates in matrix semantics
- A note on natural extensions in abstract algebraic logic
- THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
- A Generalization of Maksimova’s Criterion for the Disjunction Property
- A Henkin-style proof of completeness for first-order algebraizable logics
- THE LATTICE OF SUPER-BELNAP LOGICS
- The algebraic significance of weak excluded middle laws
- Logics of upsets of De Morgan lattices
- A general Glivenko-Gödel theorem for nuclei
- A gentle introduction to the Leibniz hierarchy
- Conservation as translation
- Intuitionistic Sahlqvist theory for deductive systems
- Algebraic proof theory: hypersequents and hypercompletions
- De Morgan clones and four-valued logics
- Logics with disjunction and proof by cases
This page was built for publication: The proof by cases property and its variants in structural consequence relations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q368486)
