The proof by cases property and its variants in structural consequence relations (Q368486): Difference between revisions

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.