How Many Theorems (Tautologies) Exist of 5, 6, 7, 8, and 9 Letters? Suppose we only have the material conditional C and logical negation N for a system of propositional calculus, with only variables and no constants in any formula.  Suppose that formulas like Cpq aren't considered distinct from Cxy or Crs or Cab, though Cpp does get considered distinct from Cpq (I don't know how to define this exactly).  With that in mind, there don't exist any theorems of one letter, or two letters, and the only theorem of three letters is Cpp.  There are no theorems of four letters since none of {NCpq, NCpp, CpNq, CNpq, CpNp, CNpp} are theorems (unless I've missed a possibility).  How many theorems exist of 5, 6, 7, 8, 9 letters?  Since "combinatorial explosion" seems to happen here, what sort of methods can one use to attack such a problem?
 A: To solve for the general case, solve a system of generating functions. One function in the system will represent the number of ways of computing one boolean function $f$ as a sequence of $d$ characters from C, N, p, q, the number for length $d$ being the coefficient of $z^d$ in $f$.
The system of gfs is one definition of a generating function for every logical function on two variables. And each definition will have terms to correspond to how you can compute the boolean function using the two connectives and two variables.
For convenience, let the label of a function be spelled out as the truth table of that function, and the result of an operation is pairwise. 
For example, since TFTT (the boolean function corresponding to 'p implies q', can be gotten only by C TTFF TFTF or N FTFF, the gf for the function TFTT is 
$$TFTT(z) = z TTFF(z) TFTF(z) + z FTFF(z)$$
because $z$ increments the exponent for the character C and also for the character N. 
So you'll have a system of sixteen equations, one for each boolean function on 2 variables, with only the base cases being for TTFF(z) and TFTF(z) for p and q respectively. The grammar of constructions for the entire set is context free, because the syntax of C and N is context free and the semantics of boolean functions is compositional.
I have feeling this system won't simplify very practically because it won't be particularly sparse. For example, TTTT(z), representing all theorems, is from N FFFF or C TTTT TTTT or C TTTF TTTT or C TTFT TTTT or ...
There might be a pattern to exploit to eliminate some variables systematically, or one could use Groebner Bases to do it to solve blindly (with a computer algebra package).
To see how bad it is with 2 variables start with just 1 variable. 
TT = N FF or C TT TT or C TF TT or C TF TF or C FT TT or C FF FT or C FF TT or C FF TF or C FF FT or C FF FF
To really solve the system will get you a generating function from which one might have some computational difficulty extracting coefficients. Instead, to get values manageably one can simply substitute polynomials of degree $n$, and compute, resubstituting in the new polynomials (truncating any degree generated over $n$), until it stops changing (similar to Gauss Jordan style solution of a matrix equation).
