How Many Theorems (Tautologies) Exist of 5, 6, 7, 8, and 9 Letters?

Question

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?

Answer 1

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.

Answer 2

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