Axiomatising Specification Theory

In contrast to the more usual algebraic or model theoretic approaches we can try and capture our intuitions about specification on a purely syntactic or proof theoretic level. Such intuitions are, we feel, independent of any specific logic. So we can start with the general notion of a logic as something given by a consequence relation, ⊢, as opposed to by an institution say, and investigate what we need to add, by way of properties on ⊢, in order to support an account of specification. We don’t regard such a “semantics-less” approach to be worthless but rather, in the spirit of Frege and more recently Martin-Lof, take meaning to be something that is given directly by such a proof theory.