Interpolation in computing science: The semantics of modularization (Q1024120)

Inspired by ``Module algebra'' [\textit{J. A. Bergstra}, \textit{J. Heering} and \textit{P. Klint}, J. Assoc. Comput. Mach. 37, No.~2, 335--372 (1990; Zbl 0696.68040)], the author introduces Theory Algebra (TA), an algebraic theory of logical theories with three operations: union, hiding and application of interpretations, where a \textit{theory} is a set of sentences and \textit{union} is, accordingly, set-theoretical union. Furthermore, \textit{hiding} a vocabulary \(\Sigma\) from a theory \(S\), \(\exists \Sigma \;S\), is defined as \(\{A\mid S\vdash A\) and \(\text{VOC}(A)\cap\Sigma =\emptyset\}\), where a \textit{vocabulary} is a set of predicate and function symbols, while \(\text{VOC}(A)\) is the set of predicate and function symbols appearing in formula \(A\). Finally, an \textit{interpretation} is a structure-preserving mapping on terms and formulas, mapping predicate (function) symbols to predicate (function) symbols of the same arity. The main results are the following. Modularization: For theories \(S\), \(T\), \(U\) and an interpretation \(\kappa\) (and further technical hypotheses on the vocabularies), if \(T\) is a conservative extension of \(S\) and if \(S\buildrel{\kappa}\over{\to}U\), then there is a minimal \(V\) such that \(V\) is a conservative extension of \(U\) and \(T\buildrel{\kappa}\over{\to} V\). Factorization: If \(T\vdash S\), then there is a \(U\) such that \(T\) is a conservative extension of \(U\), \(U\vdash S\) and \(\text{VOC}(U)= \text{VOC}(S)\). Finally, with the \textit{export} operator \(\Sigma \boxdot S\) being defined as \(\{A\mid S\vdash A\) and \(\text{VOC}(A)\subseteq\Sigma\}\): Normal form: Expressions built from theories with the operators \(\cup\), \(\exists\) and \(\boxdot\) can be rewritten with no \(\boxdot\) and at most one occurrence of \(\exists\) (or no \(\exists\) and at most one occurrence of \(\boxdot\)). The author notes that while TA was developed with predicate logic as the underlying logic, his results will hold with any logic which satisfies reflexivity and transitivity of \(\vdash\), preservation of \(\vdash\) under interpretations and the deduction and interpolation properties.