 When one is setting up a logistic system, the well-formed expressions, axioms and rules of inference must all be specified effectively in order that there can be an effective test of whether a purported proof is really a proof. Intuitively, the requirement is that one can test—by looking at the symbols and following a fixed set of instructions for performing concrete operations with symbols—whether a given finite sequence of symbols is a wff, or whether a given finite sequence of wffs is a proof of the last wff in the sequence. In the absence of such a method.