SYMBOLS, FORMULAS, AND WFFS
The logic we have pursued so far has been concerned with arguments and statements. We have also dealt with abstract arguments, where capital letters stand for statements, and with formulas representing compound statements, argument forms, proofs, and rules of inference.
The latter were formulated in terms of statement variables, as were the argument forms we encountered in the last chapter and whose validity we proved, and there we even came across an argument form in which a conclusion was validly proved from no premises. Now it is time to bring some order to this zoo, by approaching it all systematically.We already defined argument and statement above in chapters 1 and 2. But we did not define formula. A formula is just a string of logical symbols, and when these are ordered
Each of the following is a logical symbol:
a capital letter such as A, B, R, W
Now since we know a well-formed formula must correspond to a statement, simple or compound, we may use the rules of statement formation from chapter 3 to define it. The standard abbreviation is “wff,” as pronounced by dogs:
Well-formed Formulas (wffs)
1) (simple statements) Any capital letter is a wff.
2) (unary compounds) A wff preceded by a negation symbol is a wff.
3) (binary compounds) A left-hand grouper, followed by a wff, followed by a binary operator, followed by a wff, followed by a matching right-hand grouper, is a wff.
3*) (convention regarding outermost groupers) The outermost groupers are understood, and need not be explicitly written in (although they can be).
4) Only formulas that are Constructible by application of the above three rules are wffs.
The above is what’s called a recursive definition; once we have something that’s a wff by clause 1) we can plug it into clause 2) or 3) wherever the word wff appears and generate another wff, and so on recursively.
Conversely, if we have a formula and want to see whether it is a wff, we see if we can build it up by the above rules: it will be a wff if and only if it can be built up by these rules. Let’s look at some examples to see how this works:
A, B.,. C This is not a wff, because the comma and triple-dot do not occur in the definition of wffs.
This definition of wffs can be useful in helping to properly identify statements as negations, conditionals, etc., and thus in applying rules of inference without making mistakes. Take, for instance, the following “proof’ of an instance of one of De Morgan’s Laws using only rules of inference other than DM:
I leave the blunder on line (4) for you to identify. Here Γm interested in the error on line 
as what we have called an abstract argument: this is what we get when we take an argument in words (a concrete argument) and symbolize it. That is, each constituent statement of the argument is symbolized by representing it by a wff. It is then an interpreted statement. Thus
An abstract argument is what is obtained by symbolizing an argument. The premises are represented as wffs separated by commas; they are followed by the triple-dot symbol, and a wff symbolizing the conclusion, e.g.,
Analogously,
An abstract statement is what is obtained by symbolizing a statement. It is simply an interpreted wff.[LIII]
Now, in analyzing arguments we found that certain patterns often recurred, and in stating these patterns we found it convenient to introduce statement variables, which stand for any abstract statements that we may consistently substitute for them.
ThusA statement variable is any lower-case italicized letter from p to z that is used as a place-holder for statements, i.e., for which any abstract statement may be substituted.
We used these statement variables to express argument forms:
An argument form is an array of logical symbols containing statement variables rather than statements, such that a single-inference argument is produced when statements are consistently substituted for the variables,
Obviously the components of such argument forms are likewise not statements, but are themselves forms:
A statement form is an array of logical symbols containing statement variables such that an abstract statement or wff is produced when statements or wffs are consistently substituted for the variables,
A substitution instance of an argument form is any argument that results when the same statement or wff is substituted for each occurrence of the same statement 
A proof of the vahdity of an argument form is a numbered sequence of Hnes, each of which contains either a premise of an argument of this form, a supposition, or a statement derived from one of the preceding Hnes by a rule of inference; and whose last line is the conclusion of the argument, occurring after all suppositions have been discharged.
12.1.2