 For the second observation, we note a more linguistic reformulation of Rautenberg’s result, for which we first need a brief digression on defined connectives. A connective derived by composition from a set of primitive connectives yields a defined connective in one of two ways, depending on one’s views of definition. On one view, isolating the derived connective is already giving a definition: one has a formula φ(p1,…, pn) in which exactly the exhibited variables occur, which since it is constructed from these variables via the primitive connectives constitutes a derived connective, applying to formulas ψ1,…, ψn to yield the formula φ(ψ1,…,ψn) which results from substituting ψi uniformly for pi in φ(p1,…, pn). We can introduce a shorthand to such substitution-instances, denoting φ(ψ1,…,ψn) by “#(ψ1,…,ψn)”, for instance—as in calling the formula ¬(ψ1 ∧ ¬ ψ2) by the name “ψ1 → ψ2”. (Of course this would only be a good idea if there is nothing better to mean, or which is already meant, by →—as there would be in intuitionistic logic, for instance.) That is the first view of  definition.[13]  On the second view, rather than just being a metalinguistic abbreviation, the defined connective is an addition to the object language: we add (to continue with the example just given) a new primitive connective →, along with a stipulation that compounds of the form ψ1 → ψ2 are to be synonymous with those of the corresponding form ¬(ψ1 ∧ ¬ ψ2). We need not choose between these views here, but some formulations are sensitive to which view is taken. In particular, if we have classical logic with primitives ¬ and ∧, we may still wish to consider its implicational fragment—in Set-Fmla, say, where this would be the restriction of ⊢CL to formulas constructed using only the connective →. On the first view of definition, we cannot literally do that, since to use → is ipso facto to use ¬ and ∧, so what is meant is rather than the only occurrences of ¬ and ∧ are such as occur in subformulas of the form ψ1 → ψ2 in virtue of these being the formulas ¬(ψ1 ∧ ¬ψ2). On the second view of definition, we have expanded the language-as-algebra by adding a new fundamental operation → and can now consider the subalgebra generated by the propositional variables of the reduct of this algebra obtained by discarding the other fundamental operations.