The proof by cases property and its variants in structural consequence relations (Q368486)

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.