New
Elegant Axiomatizations of Some Sentential Logics
Branden
Fitelson1
Table of
Contents
- 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
1 Left Group
Calculus
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):
- 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:
- Lukasiewicz's student Mordchaj Wajsberg [37]
later discovered the following organic4
23-symbol single axiom for D:
- Lukasiewicz later discovered another 23-symbol organic axiom:
- We have discovered many new 23-symbol single axioms, some of
which are organic and have only 4 variables, e.g.,
- 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
- 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.
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.