A semantic approach to conservativity (Q284219)

If \(\mathsf T\) is a set of first-order sentences, then \(\mathsf T^c\) and \(\mathsf T^i\) are closures of \(\mathsf T\) under classical and intuitionistic derivability, respectively. \(\mathsf T^c\) is conservative over \(\mathsf T^i\) with respect to a class of formulae \(\Gamma\) iff \(\mathsf T^c\) and \(\mathsf T^i\) contain the same formulae in \(\Gamma\). In the paper, the problem of conservativity is described from a semantical point of view. A Kripke model \(\mathcal M\) is called \(\mathsf T^c\)-normal if every world in \(\mathcal M\) is a classical model of \(\mathsf T^c\). The class of formulae \(\mathcal P(\mathsf T^i)\) is defined as the smallest class that contains all atomic formulae, all formulae decidable in \(\mathsf T^i\) and is closed under disjunctions, conjunctions and existential quantification. The class of formulae \(\mathcal G(\mathsf T^i)\) is the smallest extension of \(\mathcal P(\mathsf T^i)\) closed under the following rules: \begin{itemize} \item[1)]~if \(B,C\in\mathcal G(\mathsf T^i)\), then \(B\land C,B\lor C,\exists x\,B,\forall x\,B\in\mathcal G(\mathsf T^i)\); \item[2)] if \(B\in\mathcal P(\mathsf T^i)\) and \(C\in\mathcal G(\mathsf T^i)\), then \(B\to C\in\mathcal G(\mathsf T^i)\). \end{itemize} The class \(\mathcal A(\mathsf T^i)\) is defined as the class of formulae of the form \(\forall\bar x\,(C(\bar x)\to\forall y\,D(\bar x,y))\), where \(C\in\mathcal G(\mathsf T^i)\) and \(D\in\mathcal P(\mathsf T^i)\). The first main result is Theorem 4.10. If \(\mathsf T^i\) is complete with respect to a class of \(\mathsf T^c\)-normal Kripke models, then \(\mathsf T^c\) is conservative over \(\mathsf T^i\) with respect to the class \(\mathcal A(\mathsf T^i)\). This result provides a new proof of \(\Pi_2\)-conservativity of \(\mathsf{PA}\) over \(\mathsf{HA}\), that can be proved by the negative translation together with the Friedman translation. Another consequence is \(\Pi_2\)-conservativity of the fragment \(\mathsf i\Delta_0\) of \(\mathsf{PA}\), where induction is restricted to bounded formulae, over its intuitionistic counterpart. The second main result is Theorem 5.6. If \(\mathsf T^i\) is closed under the Friedman translation and complete with respect to a class of conversely well-founded Kripke models, then \(\mathsf T^c\) is conservative over \(\mathsf T^i\) with respect to the class of formulae of the form \(\forall x\exists y\,A\), where \(A\in\mathcal P(\mathsf T^i)\). If, in addition, \(\mathsf T^i\) is complete with respect to a class of conversely well-founded Kripke models with constant domains, then \(\mathsf T^c\) is conservative over \(\mathsf T^i\) with respect to the class of prenex formulae whose matrix is built from atoms by means of disjunctions and conjunctions. Applications of the presented results to the constructive set theory \(\mathsf{CZF}\) are considered.