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?

-
Somewhat related: oeis.org/A166746 –  Gerry Myerson Oct 17 '11 at 2:52
Generate and test? That is, write a program to generate all possible wffs, and then do a truth table on each one. –  Mitch Oct 17 '11 at 3:01
@Mitch I know next to nothing about programming. You'd need to make sure the program "regards" Cpq and Cxy as "the same." I think you can get around that by changing the alphabet for the number of letters involved (if I've got my terms straight). Since C is binary, it follows that for 1, 2, your alphabet is {p} (or any singleton). For 3 or 4 letters your alphabet is {p, q}. For 5 or 6 letters your alphabet is {p, q, r}. For 7 or 8 letters your alphabet is {p, q, r, s}. And for 9 or 10 letters your alphabet is {p, q, r, s, t}, and so on. But, how do you generate all possibilities? –  Doug Spoonwood Oct 17 '11 at 3:11
@Doug: you do not seem to know how to treat the general case, so it is a rather sensible suggestion that you consider the simpler case in which there are only two variables first. –  Mariano Suárez-Alvarez Oct 17 '11 at 4:41
A nice question is: «how complicated is the language of all tautologies involing $\implies$, $\neg$ and the two variables $x$ and $y$?» Is it context-free, for example? (One would probably have to write the operators infixly for this) Better: is it regular? See math.stackexchange.com/q/73274/274 –  Mariano Suárez-Alvarez Oct 17 '11 at 6:43

The 290 tautologies in at most 8 symbols, up to $\alpha$-equivalence, are:

C11       C1C11     C1C22     C2C12     C1NN1
CN1N1     CNN11     NNC11     C1CN11    C2CN21
C2CN12    CN1C11    CN1C22    CN2C21    CCN111
CNC111    CNC221    CNC212    CNC212    C1C1C11
C1C2C22   C2C1C22   C2C2C12   C1C1C22   C1C2C12
C1C2C21   C1C2C33   C1C3C23   C3C1C23   C1C1NN1
C1C2NN2   C2C1NN2   C1CN1N1   C1CN2N2   C2CN2N1
C1CC111   C2CC122   C2CC122   C2CC212   C2CC212
C1CC221   C1CC122   C1CC122   C3CC123   C1CNN11
C1CNN22   C1CNN22   C2CNN12   C1NC1N1   C1NNC11
C1NNC22   C2NNC12   C1NNNN1   CN1C1N1   CN2C1N2
CN2C2N1   CN1NNN1   CC11C11   CC12C22   CC21C22
CC11C22   CC12C12   CC12C33   CNN1C11   CNN2C12
CNN2C12   CNN1C22   CNN1NN1   CC1N1N1   CNC11N1
CNC22N1   CNC12N2   CNC12N2   CNNN1N1   CCC1111
CCC2122   CCC2122   CCC2211   CCC2211   CNC1N11
CNC1N22   CNC1N22   CNC2N12   CNC2N12   CNNNN11
NNC1C11   NNC1C22   NNC2C12   NNC1NN1   NNCN1N1
NNCNN11   NNNNC11   C1C1CN11  C1C2CN22  C1C2CN22
C2C1CN22  C2C1CN22  C2C2CN21  C2C2CN12  C1C2CN21
C1C2CN12  C1C3CN32  C1C3CN23  C3C1CN32  C3C1CN23
C1CN1C11  C1CN2C22  C2CN1C22  C2CN2C12  C2CN2C21
C1CN1C22  C1CN2C21  C1CN2C33  C1CN3C32  C3CN1C23
C3CN3C12  C1CN1NN1  C2CN1NN2  C2CN2NN1  C1CC1N11
C2CC2N21  C2CC1N22  C2CC1N22  C2CC2N12  C2CC2N12
C1CC2N21  C3CC1N23  C1CCN111  C1CCN222  C1CCN222
C2CCN212  C2CCN212  C2CCN122  C2CCN122  C1CCN221
C1CCN221  C3CCN213  C1CNC111  C1CNC222  C1CNC222
C2CNC221  C2CNC122  C2CNC122  C2CNC212  C2CNC212
C1CNC221  C1CNC212  C1CNC212  C1CNC332  C1CNC323
C1CNC323  C3CNC231  C3CNC123  C1CNNN11  C2CNNN21
C2CNNN12  C1NNCN11  C2NNCN21  C2NNCN12  CN1C1C11
CN1C2C22  CN2C1C22  CN2C2C12  CN2C2C21  CN1C1C22
CN1C2C12  CN1C2C33  CN1C3C23  CN3C1C32  CN3C3C12
CN1C1NN1  CN1C2NN2  CN2C2NN1  CN1CN1N1  CN1CN2N2
CN2CN1N2  CN1CNN11  CN1CNN22  CN1CNN22  CN2CNN21
CN1NCN11  CN1NNC11  CN1NNC22  CN2NNC21  CNN1CN11
CNN2CN21  CNN2CN12  CNN2CN12  CC1N1C11  CC1N2C22
CC1N2C22  CC2N2C21  CC2N2C21  CC2N1C22  CC1N1C22
CC1N2C33  CCN11C11  CCN21C22  CCN21C22  CCN22C12
CCN22C12  CCN12C22  CCN11C22  CCN22C11  CCN21C33
CCN11NN1  CNC11C11  CNC22C12  CNC22C12  CNC22C21
CNC22C21  CNC12C22  CNC12C22  CNC21C22  CNC21C22
CNC22C11  CNC21C12  CNC12C21  CNC33C12  CNC32C13
CNC32C13  CNC23C31  CNC23C31  CNC12C33  CNC11NN1
CNC21NN2  CNC22NN1  CNNN1C11  CNNN2C21  CNNN2C21
CNNN1C22  CNCN11N1  CNCN21N2  CNCN21N2  CNCN12N2
CNCN12N2  CCN1NN11  CCC1N111  CCC1N222  CCC1N222
CCC2N122  CCC2N122  CCNNN111  CNC1C111  CNC2C221
CNC1C222  CNC1C222  CNC2C122  CNC2C122  CNC2C212
CNC2C212  CNC1C221  CNC2C121  CNC1C221  CNC1C212
CNC2C331  CNC3C231  CNC1C323  CNC1C323  CNC3C123
CNC3C123  CNC1NN11  CNC2NN21  CNC2NN12  CNC2NN12
CNCN1N11  CNCN2N21  CNCN1N22  CNCN1N22  CNCNN111
CNCNN221  CNCNN221  CNCNN212  CNCNN212  CNNCN111
CNNNC111  CNNNC221  CNNNC212  CNNNC212  NNC1CN11
NNC2CN21  NNC2CN12  NNCN1C11  NNCN1C22  NNCN2C21
NNCCN111  NNCNC111  NNCNC221  NNCNC212  NNCNC212


There are 1113 more with exactly 9 letters.

I generated the above list with the following Mathematica code:

partitions[{}] := {{}};
partitions[l_] := Union@Flatten[Table[
Sort@Prepend[p, s],
{s, Subsets[l, {1, \[Infinity]}]}, {p,
partitions[Complement[l, s]]}
], 1]

shapes[l_ /; l <= 0] := {};
shapes[1] := {var[]};
shapes[l_] := Join[
Flatten[
Table[imp[a, b], {i, 1, l - 1}, {a, shapes[i]}, {b, shapes[l - i - 1]}],
2],
Table[neg[a], {a, shapes[l - 1]}]
]

label[w_] := Table[
ReplacePart[w,
Flatten[MapIndexed[Function[{q, i}, # -> var[i[[1]]] & /@ q], p, 1], 1]],
{p, partitions[Position[w, var[]]]}
]

formulas[l_] := Flatten[label /@ shapes[l], 1]

lessPretty[imp[a_, b_]] := "C" <> lessPretty[a] <> lessPretty[b];
lessPretty[neg[a_]] := "N" <> lessPretty[a];
lessPretty[var[]] := "\[CenterDot]";
lessPretty[var[i_]] := ToString[i];

neg[x_] := ! x /; x \[Element] Booleans;
imp[x_, y_] := x \[Implies] y /; {x, y} \[Element] Booleans;

tautologyQ[w_] := Module[{vars = Union@Cases[w, var[i_], \[Infinity]]},
And @@ Map[
w /. MapThread[Rule, {vars, #}] &,
Tuples[{False, True}, Length[vars]]
]
]

tautologies = Select[Flatten[formulas /@ Range[1, 8]], tautologyQ];
output = StringJoin[Table["* " <> lessPretty[t] <> "\n", {t, tautologies}]];
WriteString["/tmp/formulas", output];
Close["/tmp/formulas"];


Using this code, one computes in a couple of minutes that the sequence counting tautologies starts with $$0, 0, 1, 0, 7, 11, 73, 198, 1113, 3755, 18957, 75723, \dots$$ This is not in the EOIS.

-
Many of these have $NNi$ inside them or are of the form $C(\text{something})(\text{some shorter tautology})$. If this is going to become minimally interesting, one should count only «minimal» tautologies in some sense... –  Mariano Suárez-Alvarez Oct 17 '11 at 3:53
You might find the service provided by pastebin.com useful for answers like these. –  anon Oct 17 '11 at 4:02
(Someone should submit the sequence to the OEIS...) –  Mariano Suárez-Alvarez Oct 17 '11 at 5:42
Above you say you get 290 for 8 vars, but in the sequence at the bottom you give 198. Which is it? –  Mitch Oct 17 '11 at 14:43
@Mitch: I wrote «at most $8$ symbols», and that is precisely what I meant :) $1+7+11+73+198=290$. –  Mariano Suárez-Alvarez Oct 17 '11 at 14:46

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 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).