`Left Group Calculus``Classical Sentential Logic --- In the Sheffer Stroke (D)``Classical Sentential Logic --- In Implication (C) and The False (O)``The Implicational Fragment (C5) of the Modal Logic S5``The Implicational Fragment (C4) of the Modal Logic S4``The Implicational Fragment (RM`_{→}`) of the "Classical" Relevance Logic RM``Single Axioms for the Implicational Fragments of Some Other Non-Classical Logics``Automated Reasoning Techniques Used`

- Let the operation Eab correspond to
left division a
^{-1}b 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):

(L

_{1}) EEEpEEqqprr(L

_{2}) EEEEEpqEprEqrss(L

_{3}) EEEEEEpqEprsEEqrstt(L

_{4}) EEEEpqrsEEEptrEEqts(L

_{5}) EEEpEEqprEEsptEEEEpqsrt

- With OTTER, McCune [13]
showed (
*inter alia*) that L_{1}, L_{4}, L_{5}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.

- In 1917, Nicod [21]
showed
^{3}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
*organic*^{4}23-symbol single axiom for D:

DDpDqrDDDsrDDpsDpsDpDpq

- Lukasiewicz later discovered another 23-symbol organic axiom:

DDpDqrDDpDrpDDsqDDpsDps

_{2}

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

- 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}^{ }

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

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

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

CCCCCpqrCqprr ^{6}^{ } - 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).

- 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,_{→}*in*organic 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 Eand 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 one_{→}^{7}) has at least 25 symbols.

- The shortest single axiom for E

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

- 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}

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

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

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

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

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

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

^{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.