New Elegant Axiomatizations of Some Sentential Logics

Branden Fitelson1

Table of Contents

  1. Left Group Calculus
  2. Classical Sentential Logic --- In the Sheffer Stroke (D)
  3. Classical Sentential Logic --- In Implication (C) and The False (O)
  4. The Implicational Fragment (C5) of the Modal Logic S5
  5. The Implicational Fragment (C4) of the Modal Logic S4
  6. The Implicational Fragment (RM→) of the "Classical" Relevance Logic RM
  7. Single Axioms for the Implicational Fragments of Some Other Non-Classical Logics
  8. Automated Reasoning Techniques Used

 

1 Left Group Calculus

  • Let the operation Eab correspond to left division a-1b in groups. Kalman [3] shows that the following is an equational 2-basis for group theory:

    EExEyyEzz = x

           EExyExz = Eyz

  • It is also shown in [3] that the following is a 5-axiom logical calculus (assuming condensed detachment as the sole rule of inference) for groups (i.e., a = b is a theorem of group theory iff both Eab and Eba are derivable from the following five axioms using only condensed detachment as the sole rule of inference):

    (L1) EEEpEEqqprr

    (L2) EEEEEpqEprEqrss

    (L3) EEEEEEpqEprsEEqrstt

        (L4) EEEEpqrsEEEptrEEqts

    (L5) EEEpEEqprEEsptEEEEpqsrt

  • With OTTER, McCune [13] showed (inter alia) that L1, L4, L5 are dependent, and that the following 27-symbol formula is a single axiom for LG:

    EEEEpqrEEstEEEutEusvErEEqpv

  • Recently, we found the following 23-symbol axiom for LG (and several others of the same length):

    EEEpqrEEEspEEEtuEqsEutr

    Open Question: Is there a shorter single axiom for LG? The 11-symbol formula EEpqEEprEqr cannot be ruled-out using only finite models.

2 Classical Sentential Logic --- In the Sheffer Stroke (D)

  • In 1917, Nicod [21] showed3 that the following 23-symbol formula (in Polish notation) is a single axiom for classical sentential logic (D is interpreted semantically as NAND, i.e., the Sheffer stroke):

    DDpDqrDDtDttDDsqDDpsDps


  • The only rule of inference for Nicod's single axiom system is the following, somewhat odd, detachment rule for D:

    From DpDqr and p, infer r.


  • Lukasiewicz [7] later showed that the following substitution instance (t/s) of Nicod's axiom (N) would suffice:

    DDpDqrDDsDssDDsqDDpsDps


  • Lukasiewicz's student Mordchaj Wajsberg [37] later discovered the following organic4 23-symbol single axiom for D:

    DDpDqrDDDsrDDpsDpsDpDpq


  • Lukasiewicz later discovered another 23-symbol organic axiom:

    DDpDqrDDpDrpDDsqDDpsDps2


  • We have discovered many new 23-symbol single axioms, some of which are organic and have only 4 variables, e.g.,

    DDpDqrDDpDqrDDsrDDrsDps


  • We can now report that the shortest single axioms for these Sheffer Stroke systems contain 23 symbols. No shorter axioms exist.

3 Classical Sentential Logic --- In Implication (C) and The False (O)

  • Meredith [18,16] reports two 19-symbol single axioms for classical sentential logic (using only the rule of condensed detachment) in terms of implication C and the constant O (semantically, O is ``The False''):

    CCCCCpqCrOstCCtpCrp
    CCCpqCCOrsCCspCtCup

     
  • Meredith [18] claims to have ``almost completed a proof that no single axiom of (C,O) can contain less than 19 letters.'' As far as we know, no such proof was ever completed (that is, until now...).

  • We have performed an exhaustive search/elimination of all (C,O) theorems with fewer than 19 symbols. We have proven Meredith's conjecture: no single axiom of (C,O) can contain less than 19 letters.5

4 The Implicational Fragment (C5) of the Modal Logic S5

  • In their classic paper [6], Lemmon, Meredith, Meredith, Prior, and Thomas present several axiomatizations (assuming only the rule of condensed detachment) of the system C5, which is the strict implicational fragment of the modal logic S5.

  • Bases for C5 containing 4, 3, 2, and a single axiom are presented in [6]. The following 2-basis is the shortest of these bases. It contains 20 symbols, 5-variables, and 9 occurrences of the connective C.

    Cpp
    CCCCpqrqCCqsCtCps

  • The following 21-symbol (6-variable, 10-C) single axiom (due to C.A. Meredith) for C5 is also reported in [6]:

    CCCCCttpqCrsCCspCuCrp

  • We searched both for new (hopefully, shorter than previously known) single axioms for C5 and for new 2-bases for C5.

  • We discovered the following new 2-basis for C5, which (to the best of our knowledge) is shorter than any previously known basis (it has 18 symbols, 4 variables, and 8 occurrences of C):

    Cpp
    CCpqCCCCqrsrCpr

  • Moreover, we discovered the following new 21-symbol (6-variable, 10-C) single axiom for C5 (as well as 5 others, not given here):

    CCCCpqrCCssqCCqtCuCpt

  • No formula with fewer than 21 symbols is a single axiom for C5. And, no basis for C5 whatsoever has fewer than 18 symbols.

5 The Implicational Fragment (C4) of the Modal Logic S4

  • C4 is the strict-implicational fragment of the modal logic S4 (and several other modal logics in the neighborhood of S4 - see Ulrich's [34]).

     
  • As far as we know, the shortest known basis for C4 is due to Ulrich (see Ulrich's [34]), and is the following 25-symbol, 11-C, 3-axiom basis:

    Cpp
    CCpqCrCpq
    CCpCqrCCpqCpr

  • Anderson & Belnap [1] state the finding of a (short) single axiom for C4 as an open problem (as far as we know, this has remained open). The following is a 21-symbol (6-variable, 10-C) single axiom for C4:

    CCpCCqCrrCpsCCstCuCpt

  • We have also the following 20-symbol 2-basis for C4:

    CpCqq        CCpCqrCCpqCsCpr

  • No formula with fewer than 21 symbols is a single axiom for C4. And, no basis for C4 whatsoever has fewer than 20 symbols.

6 The Implicational Fragment (RM→) of the "Classical" Relevance Logic RM

  • The ``classical'' relevance logic R-Mingle (RM) was first carefully studied by Dunn in the late 60's (e.g., in [2]). Interestingly, the implicational fragment of R-Mingle (RM→) has an older history.

  • RM→ was studied (albeit, unwittingly!) by Sobocinski in the early 50's. Sobocinski [30] discusses a two-designated-value-variant of Lukasiewicz's three-valued implication-negation logic (I'll call Sobocinski's logic S). Sobocinski leaves the axiomatization of S→ as an open problem.

  • Rose [26,27] solved Sobocinski's open problem, but his axiomatizations of S→ are very complicated and highly redundant (see Parks' [23]).

  • Meyer and Parks [19,24] report an independent 4-axiom basis for S→. They also show that S→ = RM→, thus providing an independent 4-basis for RM→. Meyer and Parks show that RM→ can be axiomatized by adding the following ``unintelligible'' 21-symbol formula to R→:

    CCCCCpqqprCCCCCqppqrr

  • In other words, the following is a 5-basis for RM→:

    Cpp

    CpCCpqq

    CCpqCCrpCrq

        CCpCpqCpq

    CCCCCpqqprCCCCCqppqrr


  • The reflexivity axiom Cpp is dependent in the above 5-basis. The remaining (independent) 4-basis is the Meyer-Parks basis for RM→.

  • After much effort (and, with valuable assistance from Bob and Larry), we discovered the following 13-symbol replacement for Parks' 21-symbol formula (we've also shown that there are none shorter):

    CCCCCpqrCqprr6

  • The contraction axiom CCpCpqCpq is dependent in our new 4-basis. The remaining (independent) 3-basis for RM→ contains 31 symbols and 14 C's (the Meyer-Parks basis has 4 axioms, 48 symbols, and 22 C's).

7 Single Axioms for the Implicational Fragments of Some Other Non-Classical Logics

  • It was shown by Rezus [25] (building on earlier seminal work of Tarksi and Lukasiewicz [8]) that the systems E→, R→, and L→have single axioms. However, applying the methods of [25] yields very long, inorganic single axioms. As far as we know, these axioms have never been explicitly written down. Here is a 69-symbol (17-variable!) single axiom for the implicational fragment of Lukasiewicz's infinite-valued logic L→(obtained using the methods of [25]):

    CCCfCgfCCCCCCCCCcdCCecCedCCaCbazzCCCCxyyCCyxxwwCCCCtuCutCutssCCqCrqpp

  • Single axioms of comparable length (i.e., containing fewer than 75 symbols) can also be generated for the relevance logics E→and R→(omitted). Here's what we know about the shortest single axioms for the systems E→, R→, L→, and RM→:
     
    • The shortest single axiom for E→has between 25 and 75 symbols.
    • The shortest single axiom for R→has between 25 and 75 symbols.
    • The shortest single axiom for L→has at most 69 symbols.
    • The shortest single axiom for RM→(if there is one7) has at least 25 symbols.

8 Automated Reasoning Techniques Used 

  1. First, we wrote computer programs to generate a large list of candidate formulas which were to be tested as axioms. For most problems, it was practical to generate an exhaustive list of all formulas with up to twenty-one symbols (we can now do these through 23 symbols).

  2. All the formulas in the list would be tested (using matrices) to see which are likely to be tautologies in the system in question.8

  3. We immediately eliminated large numbers of formulas by applying known results about axiomatizations in the various systems. For example, as reported by Lemmon et. al., every axiomatization for C5 must contain a formula with Cpp as a (possibly improper) subformula [6]. Another useful result for this purpose is the Diamond-McKinsey theorem that no Boolean algebra can be axiomatized by formulas containing less than three distinct propositional letters [1].

  4. A set of formulas was selected from the list at random. Using either SEM [40] or a program written by the authors, we found a matrix that respects modus ponens, invalidates a known axiom-basis for the system, but validates the formulas selected from the list. Such a model suffices to show that the formulas are not single axioms for the system.

  5. All the remaining formulas in the list were then tested against that matrix. Every formula validated by that matrix would be eliminated.

  6. Steps 4 and 5 were repeated until the list of candidate formulas was down to a small number, or eliminated entirely.

  7. We then use OTTER [14] (+strategies! - see [39] and [4]) to attempt to prove a known axiom basis from each of the remaining candidates.

References

 
[1] Alan Ross Anderson and Nuel D. Belnap, Jr., Entailment, Princeton University Press, Princeton, N. J., 1975, Volume I: The logic of relevance and necessity.

[2] J. Michael Dunn, Algebraic completeness results for R-mingle and its extensions, J. Symbolic Logic 35 (1970), 1-13.

 
[3] J.A. Kalman, Axiomatizations of logics with values in groups, Journal of the London Math. Society 2 (1975), 193-199.

 
[4] J.A. Kalman, Automated reasoning with Otter, Rinton Press, 2001.

 
[5] Kenneth Kunen, Single axioms for groups, J. Automat. Reason. 9 (1992), 291-308.

 
[6] E. J. Lemmon, C. A. Meredith, D. Meredith, A. N. Prior, and I. Thomas, Calculi of pure strict implication, in Philosophical Logic (J.W. Davis, ed.), D. Reidel, 1969.

 
[7] J. Lukasiewicz, Selected Works, Noth Holland, 1970.

 
[8] J. Lukasiewicz and A. Tarski, Investigations into the Sentential Calculus, (1956), Appears as chapter IV in [32].

 
[9] W. McCune, Single Axioms for Groups and Abelian Groups with Various Operations, Tech. Memo ANL/MCS-P270-1091, MCS @ ANL, Argonne, IL, 1991.

 
[10] W. McCune, Solution of the Robbins problem, J. Automat. Reason. 19 (1997), 263-276.

 
[13] W. McCune, Automated discovery of new axiomatizations of the left group and right group calculi, J. Automat. Reason. 9 (1992), 1-24.

 
[14] W. McCune, Otter 3.0 Reference Manual and Guide, Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL, 1994.

 
[15] C. A. Meredith, Equational postulates for the Sheffer stroke, Notre Dame J. Formal Logic (NDJFL) 10 (1969), no. 3, 266-270.

 
[16] C. A. Meredith and A. N. Prior, Notes on the axiomatics of the propositional calculus, Notre Dame J. Formal Logic 4 (1963), 171-187.

 
[17] C. A. Meredith and A. N. Prior, Equational logic, NDJFL 9 (1968), 212-226.

 
[18] C. A. Meredith, Single axioms for the systems (C,N), (C,O) and (A,N) of the two-valued propositional calculus, J. Computing Systems 1 (1953), 155-164.

 
[19] R.K. Meyer and Z. Parks, Independent axioms for the implicational fragment of Sobocinski's three-valued logic, Z. Math. Logik Grundlagen Math. 18 (1972), 291-295.

 
[20] B. H. Neumann, Another single law for groups, Bull. Austral. Math. Soc. 23 (1981), no. 1, 81-102.

 
[21] J.G. Nicod, A reduction in the number of primitive propositions of logic, Proc. Camb. Phil. Soc. 19 (1917), 32-41.

 
[22] R. Padmanabhan and R. W. Quackenbush, Equational theories of algebras with distributive congruences, Proc. AMS 41 (1973), no. 2, 373-377.

 
[23] Zane Parks, Dependence of some axioms of Rose, Z. Math. Logik Grundlagen Math. 18 (1972), 189-192.

 
[24] Zane Parks, A note on R-Mingle and Sobocinski's three-valued logic, Notre Dame J. Formal Logic 13 (1972), 227-228.

 
[25] Adrian Rezus, On a theorem of Tarski, Libertas Math. 2 (1982), 63-97.

 
[26] Alan Rose, A formalization of Sobocinski's three-valued implicational propositional calculus, J. Computing Systems 1 (1953), 165-168.

 
[27] Alan Rose, An alternative formalisation of Sobocinski's three-valued implicational propositional calculus, Z. Math. Logik. Grundlagen Math. 2 (1956), 166-172.

 
[28] T. W. Scharle, Axiomatization of propositional calculus with Sheffer functors, Notre Dame J. Formal Logic 6 (1965), 209-217.

 
[29] H. Sheffer, A set of five independent postulates for Boolean algebras, with application to logical constants, Trans. AMS 14 (1913), no. 4, 481-488.

 
[30] Bolesaw Sobocinski, Axiomatization of a partial system of three-value calculus of propositions, J. Computing Systems 1 (1952), 23-55.

 
[31] A. Tarski, Ein beitrag axiomatik der abelshen gruppen, Fundamenta Mathematicae 30 (1938), 253-256.

 
[32] A. Tarski, Logic, semantics, metamathematics. Papers from 1923 to 1938, Oxford at the Clarendon Press, 1956, Translated by J. H. Woodger.

 
[33] Dolph Ulrich, Local search, mimeograph of unpublished lecture notes (obtained in private correspondence of 12 March 2001).

 
[34] Dolph Ulrich, Strict implication in a sequence of extensions of S4, Z. Math. Logik Grundlag. Math. 27 (1981), no. 3, 201-212.

 
[35] Dolph Ulrich, A legacy recalled and a tradition continued, J. Automat. Reason., August 2001.

 
[36] R. Veroff, Short 2-Bases for Boolean Algebra in Terms of the Sheffer Stroke, Tech. Report TR-CS-2000-25, CS @ UNM, Albuquerque, NM, 2000.

 
[37] M. Wajsberg, Logical Works, Polish Academy of Sciences, 1977.

 
[39] L. Wos, A fascinating country in the world of computing: Your guide to automated reasoning, World Scientific, 1999.

 
[40] J. Zhang and H. Zhang, SEM: A system for enumerating models, IJCAI, 1995.

Footnotes

1 Results reported here are either the result of joint work, or the work of others associated with AR @ MCS @ ANL: Larry Wos, Bill McCune, Bob Veroff, Ken Kunen, Ken Harris, Zac Ernst, Ted Ulrich, Bob Meyer, Michael Beeson et al.

3 Actually, Nicod's original proofs are erroneous (as noted by Lukasiewicz in [7]). See Scharle's [28] for a rigorous proof of the completeness of Nicod's system.

4 A single axiom is organic if it contains no tautologous subformulae. Nicod's original single axiom (and Lukasiewicz's simplifcation of it) are non-organic, because they contain tautologous subformulae of the form DxDxx.

5 The elimination of some (C,O) candidates relied on matrices generated using local search techniques (as described by Ted Ulrich in his [33, 35]). Local search is very powerful in the context of implicational logics. It has led to many useful models.

6 The alternative 13-symbol formula CCCpCCCqprqrr will also serve this purpose.

7 Rezus's work does not apply to RM→, so whether RM→ has a single axiom remains open.

8 We say `likely to be tautologies' because C4 and C5 do not have finite characteristic matrices. Thus, we used matrices which validate all tautologies for the system, but also validate a small number of contingent formulas.