The extent to which we can grasp the content of a (non-logical) theory, expressing it economically by means of an axiom system or basis, varies greatly. In this paper we shall investigate what degree of economy, or at least regularity, can be achieved for all recursively axiomatizable first-order theories. A useful approach, also of interest in its own right, turns out to be the study of bases for subtheories, where a subtheory of a given theory consists of those theorems from which certain predicate symbols are absent. These predicate symbols might be thought of as the formal counterparts of the “purely theoretical” terms employed by a science, the theory corresponding to the science itself and the subtheory to its “observational consequences”. Roughly speaking, the types of operations involving such predicate symbols will be reduced to a minimum, so that their syntactical role in deductions will emerge more clearly.

Axiomatizations of the sentential calculus which use Rmp (modus ponens), have been shown equivalent to axiomatizations similar in all respects except that Rmp is replaced by the less restricted rule Re (rule of excision)1:

Re. If S and (…(S⊃S') …), then (… S' …).

Those who object to the identification of strict implication and entail-ment speak in such a way that for A to entail B, A must be relevant to B. This view of entailment agrees not only with that of the naive student of logic (who tends to think the phrase paradoxes of “implication” more accurate than “paradoxes” of implication), but also with that expressed in the initial chapters of many textbooks in logic under the heading “Fallacies of Relevance.”2

In regard to formal theories proposed as explications of the notion of entailment, it becomes important to have at our disposal some formal account of the demand for relevance as between antecedent and consequent of an entailment.

The notion of constructibility introduced by Gödel in [2] has been generalized by Hajnal [3], [4] in order to prove the conditional independence of the generalized continuum hypothesis and related axioms. A very similar construction was used independently by Shoenfield [11], [12]2 and the author [7] to prove the conditional independence of V = L and related axioms. Here we shall prove results further in the latter direction than those in Shoenfield [12].