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.

John Kalman's book on OTTER on page 217 has the following problem:

"In [this newsletter], Morgan essentially proposed the following problem.

Problem 8.6 Use an automatic theorem-prover to find a proof that the propositional formula CpNNp is derivable by the of condensed detachment from the propositional formulas CpCqp, CCpCqrCCpqCpr, and CCpqCNqNp."

This problem isn't solvable.  Let 0 be the designated element.  Suppose we have only two values "0" and "1", and C(0,x)=x, C(1,x)=0, and N(x)=1.  Then, CpCqp, CCpCqrCCpqCpr, and CCpqCNqNp are satisfied, but CpNNp is not.

Axiomatic proofs which prove an alternative basis for a propositional calculus can often get used to extract more axiom sets for that same propositional calculus.  Even proving a single axiom of a distinct basis can tell you about other bases which exist.

For example, let's suppose that we start with the Church-Lukasiewicz basis {CxCyx, CCxCyzCCxyCxz, CCNxNyCyx} and want to derive Lukasiewicz's preferred basis {CCxyCCyzCxz, CCNxxx, CxCNxy}.  OTTER found this proof of Clavius: CCNppp:

Length of proof is 14.  Level of proof is 6.

---------------- PROOF ----------------

1 [] P(C(x,C(y,x))).
2 [] P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
3 [] P(C(C(N(x),N(y)),C(y,x))).
4 [] -P(C(x,y))| -P(x)|P(y).
7 [] -P(C(C(N(p),p),p)).
10 [hyper,4,2,2] P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).
11 [hyper,4,2,1] P(C(C(x,y),C(x,x))).
12 [hyper,4,1,3] P(C(x,C(C(N(y),N(z)),C(z,y)))).
14 [hyper,4,1,1] P(C(x,C(y,C(z,y)))).
17 [hyper,4,11,1] P(C(x,x)).
19 [hyper,4,1,17] P(C(x,C(y,y))).
24 [hyper,4,1,19] P(C(x,C(y,C(z,z)))).
31 [hyper,4,10,14] P(C(C(x,C(C(y,x),z)),C(x,z))).
33 [hyper,4,10,24] P(C(C(x,C(C(y,y),z)),C(x,z))).
38 [hyper,4,2,12] P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).
163 [hyper,4,31,12] P(C(N(x),C(x,y))).
191 [hyper,4,2,163] P(C(C(N(x),x),C(N(x),y))).
357 [hyper,4,38,191] P(C(C(N(x),x),C(y,x))).
371 [hyper,4,33,357] P(C(C(N(x),x),x)).
372 [binary,371.1,7.1] $F.

Since we know that {CCxyCCyzCxz, CCNxxx, CxCNxy} is a basis, and CCNxxx can get derived from formulas 33 and 357 above, we can replace CCNxx by formulas 33 and 357 above to get another basis.  Doing this we find that {P(C(C(x,y),C(C(y,z),C(x,z))))., P(C(x,C(N(x),y)))., P(C(C(N(x),x),C(y,x)))., P(C(C(x,C(C(y,y),z)),C(x,z))).} is a basis.  Furthermore, formula 357 P(C(C(N(x),x),C(y,x))). can get replaced by formulas 38 and 191.  Thus, {P(C(C(x,y),C(C(y,z),C(x,z))))., P(C(x,C(N(x),y)))., P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).,  P(C(C(N(x),x),C(N(x),y)))., P(C(C(x,C(C(y,y),z)),C(x,z))).} is a basis.  Continuing this process we can infer that {P(C(C(x,y),C(C(y,z),C(x,z))))., P(C(x,C(N(x),y)))., P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).,  P(C(N(x),C(x,y)))., P(C(C(x,C(y,z)),C(C(x,y),C(x,z))))., P(C(C(x,C(C(y,y),z)),C(x,z)))}.

For many proofs of an alternative we can ask, what is the first alternative basis that gets derived in the proof?  OTTER found this proof:

Length of proof is 22.  Level of proof is 6.

---------------- PROOF ----------------


1 [] P(C(x,C(y,x))).
2 [] P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
3 [] P(C(C(N(x),N(y)),C(y,x))).
4 [] -P(C(C(p,q),C(C(q,r),C(p,r))))| -P(C(C(N(p),p),p))| -P(C(p,C(N(p),q)))|$ANS(all).
5 [] -P(C(x,y))| -P(x)|P(y).
8 [hyper,5,2,2] P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).
9 [hyper,5,2,1] P(C(C(x,y),C(x,x))).
10 [hyper,5,1,3] P(C(x,C(C(N(y),N(z)),C(z,y)))).
11 [hyper,5,1,2] P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))).
12 [hyper,5,1,1] P(C(x,C(y,C(z,y)))).
15 [hyper,5,9,1] P(C(x,x)).
17 [hyper,5,1,15] P(C(x,C(y,y))).
22 [hyper,5,1,17] P(C(x,C(y,C(z,z)))).
25 [hyper,5,1,12] P(C(x,C(y,C(z,C(u,z))))).
29 [hyper,5,8,12] P(C(C(x,C(C(y,x),z)),C(x,z))).
31 [hyper,5,8,22] P(C(C(x,C(C(y,y),z)),C(x,z))).
36 [hyper,5,2,10] P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).
79 [hyper,5,8,25] P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))).
160 [hyper,5,29,11] P(C(C(x,y),C(C(z,x),C(z,y)))).
161 [hyper,5,29,10] P(C(N(x),C(x,y))).
166 [hyper,5,2,160] P(C(C(C(x,y),C(z,x)),C(C(x,y),C(z,y)))).
189 [hyper,5,2,161] P(C(C(N(x),x),C(N(x),y))).
355 [hyper,5,36,189] P(C(C(N(x),x),C(y,x))).
369 [hyper,5,31,355] P(C(C(N(x),x),x)).
2037 [hyper,5,79,160] P(C(C(C(x,y),z),C(y,z))).
2127 [hyper,5,2037,189] P(C(x,C(N(x),y))).
14555 [hyper,5,2037,166] P(C(C(x,y),C(C(y,z),C(x,z)))).
14837 [hyper,4,14555,369,2127] $ANS(all).

I'll use numerals here.  What is the first basis derived in this proof which doesn't have any members in common with the axiom set?  {14555, 2127, 369} is the targeted basis.  Thus, {2037, 166, 2127, 369} is a basis.  So is {2037, 166, 189, 369}, {79, 160, 166, 189, 369}, {79, 160, 166, 189, 31, 355}, {79, 160, 166, 189, 31, 36}.  We don't replace 189 by its parents, since 2 is in the initial axiom set.  Nor do we replace 166 for the same reason.  {79, 29, 11, 166, 189, 31, 36} is another basis.  {8, 25, 29, 11, 166, 189, 31, 36} is another basis.  36 doesn't get replaced by its parents, but 31 does yielding {8, 25, 29, 11, 166, 189, 22, 36} as a basis.  {8, 25, 12, 11, 166, 189, 22, 36} is another basis.  Consequently, contrary to what I expected when I posed the question above, there exist a few bases which get derived at the same time.  That said, the proof of the sufficiency of the Church-Lukasiewicz basis does happen in a unique number of steps in this proof.  In other words, if we already knew about these bases, then the last 5 steps of the proof above (excluding the step which derives the empty clause) would not come as necessary to derive a distinct basis.

The following gives us a proof of ECpqANpq with an adaptation of an idea in Arthur Prior's Formal Logic p. 65-66.

First formation rules:

1. All lower case letters of the Latin alphabet are formulas.
2. If x is a formula, then δx is a formula.
3. If x is a formula, then Nx is a formula.
4. If x and y are formulas, then C x y is a formula (spaces can get ignored or inserted freely).

Let "0" stand for falsity, and "1" for truth. We have the following matrix for implication "C", disjunction (or equivalently alternation) "A", and negation "N".

C | 0  1|  A| 0  1|  N
----------------------
0 | 1  1|  0| 0  1|  1
1*| 0  1|  1| 1  1|  0

This gives us the equations C00 =1, C01=1, C10=0, C11=1, A00=0, A01=1, A10=1, A11=1, N0=1, N1=0.
δ stands for a functioral variable. Paraphrasing Prior, where x is a formula, δx stands for any truth-function into which δ enters as argument. δa stands for any truth-function of b, such as Nb, Abb, Aab, CNba, CCbcCCabCac. δb can also stand for b itself. Substitution for δ occurs by putting the argument of δ into the position where an " ' " symbol appears. The notation x/y indicates that x is to get substituted with y for all instances of x in the formula in which x appears. For example, the substitution instruction δ/C ' ' in δr yields Crr. δ/C ' A ' p in C δr δp yields C CrArp CpApp. The substitution δ/' in say C δp δ1 just has us dropping δ yielding Cp1. δ/A ' C ' ' in C δp A δq δ Na yields C ApCpp A AqCqq CNaANaNa.
Note that the valuation function "v", v(C x y)=C v(x) v(y). Also, for the valuation function v(δx)=δv(x).
Now it turns out that the following is a meta-theorem.
Meta-Theorem 1: If v(x)=v(y), then v(C δx δy)=1. In other words, if x=y, then C δx δy follows.
Demonstration: Suppose v(x)=v(y). Since v(C00)=1, and v(C11)=1, it follows that for all p, v(Cpp)=1. Substituting p/δx in Cpp we then obtain that v(C δx δx)=1. Since v(C x y)=C v(x) v(y), it then follows that C v(δx) v(δx)=1. Since v(δx)=δv(x), it then follows that C δv(x) δv(x)=1. By the initial supposition, we then obtain that C δv(x) δ v(y)=1. Since v(δx)=δv(x) we then obtain that
C v(δx) v(δy)=1. From v(C x y)=C v(x) v(y) we thus obtain that v(C δx δy)=1. Therefore, if v(x)=v(y), then v(C δx δy)=1.
The upshot here comes as that an equation like Cxy=z gives us C δz δCxy. The suggested formulas from the above equations immediately following the table along with the axioms "C δ0 C δ1 δp" and "1", and "C Cpq C Cqp Epq" give us an axiom set here.
Let the notation 1 x/y * C 2-3 indicate that in formula 1 x gets substituted with y. This matches the formula which starts with C has 2 as its next part, and 3 as its last part. We then detach formula 3. The notation 4 x/y C 5-C 6-7 indicates that 4 matches the formula C5-C6-7. Since we already have formulas 5 and 6, we thus detach formula 7.
To see how the plan of writing the deduction proceeds, I'll write out the following calculation:

                         |-C C00 AN00=C 1 AN00=C 1 A10=C 1 1=1
            |-C C0q AN0q-|
            |            |-C C01 AN01=C 1 AN01=C 1 A11=C 1 1=1
 C Cpq ANpq-|
            |            |-C C10 AN10=C 0 AN10=C 0 A00=C 0 0=1
            |-C C1q AN1q-|
                         |-C C11 AN11=C 1 AN11=C 1 A01=C 1 1=1.

Now, to write out a deduction, we can basically move left to right here. From 1, we'll deduce C11. Then from C11 we'll deduce C 1 A10. Then C 1 AN00. Then C C00 AN00. Once we get C C01 AN01, then since we have C C00 AN00, we can get C C0q AN0q. But, I'll skip some steps here which gives us a simpler proof. Here goes:
1 1.
2 C δ1 δC00.
3 C δ1 δC01.
4 C δ0 δC10.
5 C δ1 δC11.
6 C δ0 δA00.
7 C δ1 δA01.
8 C δ1 δA10.
9 C δ1 δA11.
10 C δ1 δN0.
11 C δ0 δN1.
12 C Cpq C Cqp Epq.
13 C δ0 C δ1 δp. (this is not an axiom or theorem in intuitionistic logic).

2 δ/' * C1-14

14 C00.

3 δ/' * C1-15

15 C01.

13 δ/C0' * C14-C15-16

16 C0p.

5 δ/' * C1-17

17 C11.

13 δ/C'1 * C15-C17-18

18 Cp1.

18 p/C00 * 19

19 C C00 1.

8 δ/C C00 ' * C19-20

20 C C00 A10.

10 δ/C C00 A'0 * 20-21

21 C C00 AN00.

18 p/C01 * 22

22 C C01 1.

9 δ/CC01' * C22-23

23 C C01 A11.

10 δ/C C01 A'1 * C23-24

24 C C01 AN01.

13 δ/ C C0' AN0', p/q * C21-C24-25 

25 C C0q AN0q.

16 p/AN10 * 26

26 C 0 AN10.

4 δ/C ' AN10 * C26-27

27 C C10 AN10.

18 p/C11 * 28

28 C C11 1.

7 δ/C C11 ' * C28-29

29 C C11 A01.

11 δ/C C11 A'1 * C29-30

30 C C11 AN11.

13 δ/C C1' AN1', p/q *C27-C30-31

31 C C1q AN1q.

14 δ/C C'q AN'q * C25-C31-32

32 C Cpq ANpq.

18 p/AN00 * 33

33 C AN00 1.

2 δ/C AN00 ' * C33-34

34 C AN00 C00.

18 p/AN01 * 35

35 C AN01 1.

3 δ/C AN01 ' * C35-36

36 C AN01 C01.

13 δ /C AN0' C0', p/q * C34-C36-37

37 C AN0q C0q.

6 δ/C'0 * C14-38

38 C A00 0.

11 δ/C A'0 0 * C38-39

39 C AN10 0.

4 δ/C AN10 ' * C39-40

40 C AN10 C10.

18 p/AN11 * 41

41 C AN11 1.

5 δ/C AN11 ' * C41-42

42 C AN11 C11.

13 δ/C AN1' C1', p/q * C40-C42-43

43 C AN1q C1q.

37 δ/C AN'q C'q * C37-C43-44

44 C ANpq Cpq.

 12 p/Cpq, q/ANpq * C32-C44-45

45 E Cpq ANpq.

I looked over Arthur Prior's formal logic tonight.  Let V indicate a functioral variable of one argument.  Prior's book indicates that from the following all 2-valued propositions can get derived.  Actually, 2-5 in the following can get derived form 6. under substitution for V, substitution for variables, and detachment.

1. 1

2. C V 1 C V C00.

3. C V 1 C V C11.

4. C V 0 C V C10.

5. C V 1 C V C01.

6. C V 1 C V 0 V p.

I read about definitions getting expressed via a functioral variable " V " in two-valued logic last year and realized that definitions could get expressed in n-valued or infinite-valued logic via " V ".  For example, we could express the definition of alternation (disjunction) in three-valued logic as follows:

Definition of Alternation: C V Apq V CCpqq.

I wondered if there existed a way to axiomatize a multi-valued logic via a protothetical axiom set such as the one given above by Prior.  Since truth tables work for every single finite-valued logic, it turns out that every single finite-valued logic has a protothetical axiom scheme.  Note that axiom 6 encompasses all truth values of two-valued logic.

For example of a prothetical axiom set of a multi-valued logic, three-valued Lukasiewicz logic has the following table for C and N:

C  0  1  2  N
0   2  2  2  2
1   1  2  2  1
2* 0  1  2  0

Thus, a protothetical axiom set for Lukasiewicz 3-valued logic is the following (compare the last axiom with axiom 6. of the above).

1. 1

2. C V 2 C V C00.

3. C V 2 C V C01.

4. C V 2 C V C02.

5. C V 2 C V N0.

6. C V 1 C V C10.

7. C V 2 C V C11.

8. C V 2 C V C12.

9. C V 1 C V N1.

10. C V 0 C V C20.

11. C V 1 C V C21.

12. C V 2 C V C22.

13. C V 0 C V N0.

14. C V 2 C V 1 C V 0 V p.

I tried to post the following as a question (with previous edits) on the logic section of Mathoverflow.  They've put it on hold as unclear as to what I'm asking.  Is Mathoverflow even open to such a question, which has stood as open for a long time, getting asked in the first place? 

Title:

What is the Shortest Axiom of Classical Conditional-Negation Propositional Calculus?

Suppose that we only have propositional variables and connectives. Suppose our rules of inference are detachment {Cαβ, α} ⊢ β, and uniform substitution. Suppose that we have a binary connective "C" and a unary connective "N". In 1953 C. A. Meredith found what is currently the shortest single axiom of classical C-N (Conditional-Negation) propositional calculus [p. 302 of A. N. Prior's Formal Logic indicates this and references Prior's paper " 'Single Axioms for the Systems (C, N), (C, O), and (A, N) of the Two-valued Propositional Calculus' JCS, vol. i, No. 3 (July 1953), pp. 155-64. Systems 1.5, 3.13, 6.13, 6.14.):

CCCCCpqCNrNsrtCCtpCsp.

Or using another prefix notation

→→→→→pq→¬r¬srt→→tp→sp.

So given the first notation, the formation rules are:

1. All lower case letters of the Latin alphabet, as well as any lower case letters of the Latin alphabet sub-scripted by Hindu-Arabic numerals are formulas.
2. If x is a formula, then so is Nx.
3. If x and y are formulas, then so is Cxy.
4. Nothing else is a formula in this context.

To determine what is and what is not a formula the following suffices.

1. Assign -1 to all lower case letters, as well as all lower case letters which are sub-scripted.
2. Assign 0 to N.
3. Assign 1 to C.
4. Sum the assigned numbers as you precede from left to right throughout any given string.
5. A string will qualify as a formula if and only if it either starts and ends with -1, or if it starts with a member of {0, 1} and -1 is only reached at the spot corresponding to the last letter of the string, and that string ends with -1.

Now, via the above it turns out that any formula that starts with "C", has its antecedents corresponding to the longest subformulas which have a "0" corresponding to their last letter. So looking at the above formula, we have

C  C  C  C  C  p  q  C  N  r  N  s  r  t  C  C  t  p  C  s  p
|  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |
1  2  3  4  5  4  3  4  4  3  3  2  1  0  1  2  1  0  1  0 -1

The longest subformula which ends with the first "t" is thus CCCCpqCNrNsrt. The longest subformula which ends with the second "p" is thus "Ctp", and "s" is the longest subformula corresponding to the third "0" spot. Thus, the main breaks of the formula can get located by the following "|" marks.

C|CCCCpqCNrNsrt|C|Ctp|C|s|p.

Furthermore, the main breaks of CCCCpqCNrNsrt is given by C|CCCpqCNrNsr|t, and so on.
Suppose we have a 2-valued model of C and N given by the following table:

C  0  1  N
0  1  1  1
1  0  1  0

Does there exist any shorter single axiom, which under the rules above allows us to deduce all tautologies, and only those tautologies in the 2-valued model? Does there exist another single axiom of the same length?
If there exists a unique shortest axiom up to re-symbolization of variables and connectives, what is the shortest axiom which allows us to deduce a known axiom system for classical propositional calculus, such as the following axiom set?

1. CpCqp. [p→(q→p)].
2. CCpCqrCCpqCpr. [(p→(q→r))→((p→q)→(p→r))].
3. CCNpNqCqp. [(¬p→¬q)→(q→p)].

If there exists more than one shortest axiom, what is the set of shortest axioms up to re-symbolization of variables and connectives?

The length of an axiom is defined by the number of symbols it has when fully expressed as a well-formed formula.

I started looking at the following a few days after I read J. A. Kalman's paper on condensed detachment where he uses condensed detachment on non-tautologous formulas.

In some logical systems we can obtain a propositional variable as a theorem.  For instance, if our axiom is CpCqr, then we have the following:

axiom 1 CpCqr.
D1.1   2 Cpq.
D2.2   3 p.

Since p could mean the constant false proposition "0" this means such a system can prove a false proposition.  Most logical systems I've seen can only prove tautologies for some semantics.  It turns out there exist logical systems which have non-tautologous formula, but also can't prove a propositional variable.  Here's one:

axiom 1 CCCpqqp
D1.1   2 Cpp

It turns out that if our only inference rule is condensed detachment, and CCCpqqp is our only axiom, the entire system of theorems is {CCCpqqp, Cpp}.  From Kalman's theorem that everything deducible from substitution and detachment is a substitution of a formula deducible by condensed detachment and conversely, it follows that you can't deduce a falsity just from substitution in this system.

That said, if you were to say join CCCpqqp to a system for classical logic like Lukasiewicz's preferred axiom set, then you could deduce a variable.

axiom 1 CCpqCCqrCpr
axiom 2 CpCNpq
axiom 3 CCNppp
axiom 4 CCCpqqp
D4.3   5 Np
D2.5   6 CNNpq
D6.5   7 p