On theories with the general disjunction property (Q995384)

A theory \(T\) has the disjunction property iff, for all atomic sentences \(\varphi\) and \(\psi\), \(T\vdash\varphi\vee\psi\) implies \(T \vdash\varphi\) or \(T\vdash\psi\). \(T\) has the instantiation property iff, for any collection \(\{\theta_i(x):i\in I\}\) of atomic sentences, \(T\vdash \exists\bigwedge_i\theta_i (x)\) implies the existence of a variable-free term \(t\) such that \(T\vdash \bigwedge_i\theta_i(t)\). Both properties hold for Horn clause theories. The paper defines, for arbitrary theories \(T\) and sets of formulae \(\Phi\), a so-called general disjunction property relative to \(\Phi\) which simultaneously generalizes the disjunction resp. the instantiation property (in the case of countable conjunctions). The main result is a characterization of theories \(T\) having the general disjunction property in terms of existence of a model \({\mathcal A}\) of \(T\) having an expansion \({\mathcal A}'\) by countably many new constants such that the validity of certain existential sentences (in the expanded language) in \({\mathcal A}'\) implies the provability (in the original language) of a certain universal sentence from \(T\). Note that the author uses the same symbol for provability and satisfaction. As an application, the author shows that the theory of Boolean algebras with at least one atom, while not being equivalent to a Horn theory, nevertheless admits a Horn axiomatization relative to the set of all negations of atomic formulae.