The Law of the Excluded Middle as a Special Case

Suppose we consider the law of the excluded middle in a system which only has the classical Sheffer stroke or "NAND", denoted "D".  Definitions tell us that Np := Dpp, Apq := DNpNq.  Rewriting the definitions as demodulators, and joining a clause like -Thesis(x) | Thesis(x) to the set of support, from ApNp we can use a program like Prover9 or OTTER to obtain what we might get by hand also:

DDppDDppDpp.

It turns out that this is a special case of the more general formula:

DDpqDDpqDqp.

Thus, the law of the excluded middle in a system with the Sheffer Stroke qualifies as something of a special case.

If we look at CNNpp in a system with the Sheffer stroke, with the definition Cpq := DpDqq also, we can see that it translates to

DDDppDppDpp.

DDDpqDpqDqp = DDpqDDpqDqp, since Dxy = Dyx.  Thus, CNNpp in a system with the Sheffer stroke also ends up as a special case of a more general formula: DDDpqDpqDqp.

Now, I figured both of these out, because I knew a certain tautology.  What if I didn't know it?  How could I find such a formula?  How could I find the set of most general formulas which are still tautologies?

Since if X is more general than Y (or equivalently X subsumes Y), then Y is obtainable from X via substitution alone, it follows that if a formula X is more general than formula Y (and X != Y), then one of two things holds:

1. X has the same length of Y.  Also, for each position P of a connective in X, Y has the same connective in position P in Y.  Or in other words, where X[n] indicates that nth symbol of X, if X[n] and Y[n] belong to the set of connectives, then X[n] = Y[n].  Thus, X and Y only differ in that X has more variables than Y.  The set of possibilities here is thus finite given that variables always appear in a fixed order.

2. X is shorter than Y.  Given that variables also appear in a fixed order, the set of possibilities in this case also is finite.

Since 1 and 2 are exhaustive, it follows that given a tautology Y it is possible to find the unique set of tautologies T := {X[0], ... X[n]} which are more general than Y.

What does an algorithm to find this set of more general formulas look like?

0. For the given formula Y, find each tautology which has length less than or equal to the length of Y.  Put each of these tautologies into a candidate list.

1. For each member M of the candidate list, test it to see if it subsumes Y.  If M subsumes Y, then append M to the list of tautologies T which which are more general than Y. 

Now, give Y and the set T, it is possible that some members of T subsume other members of T.  Thus, to find the set of most general tautologies S for a given tautology Y, we can

2. For each member N of T see if it subsumes any distinct member D of T.  If so, then append N to the set of most general tautologies G of Y.