Listed below are the twenty-six open questions, some old and some new, posed in A legacy recalled and a tradition continued [Journal of Automated Reasoning, vol. 27, no. 2 (2001), pp. 97-122]. Explanations of terminological and notational matters connected with each question can be found in that paper (or, alternately, on the compact disk accompanying Larry Wos and Gail Peiper's Automated reasoning and the discovery of missing and elegant proofs, Rinton Press, Paramus, 2003, where it has been reprinted with silent corrections of a few typographical errors).
          For those questions where I've learned that answers have been found or that progress has at least been made, a current status report is given.  Please e-mail me up-dated information about work on any of these questions as it becomes available: 
dulrich at purdue dot edu.

 
    QUESTION A (asked on page 105 of the "Legacy" paper, cf. page 113, and due originally to C. A. Meredith).
Is
Meredith's 21-character single axiom CCCCCpqCNrNsrtCCtpCsp / ((((p
q)(~r~s))r)t)((tp)(sp)) for classical two-valued logic using the standard connectives 'C' and 'N' shortest possible?

QUESTION B (page 106).
Is there a single axiom for classical logic in 'A' and 'N' using the rules of substitution and
disjunctive syllogism ("from A
αβ and Nα, infer β") standard in introductory logic textbooks?

UPDATE: Question B has been answered by Willemien  Hoogendoorn of Birkbeck College, London, UK, via e-mail.  She points out that the first premise of disjunctive syllogism has 'A' as main connective while the main connective of the second is 'N', so there can be no single axiom if that is the only rule permitted.  If, however, we employ also the rule "from α, infer NNα", then any one of the axioms ANANANpqArAstANANspArAtp, ANANANpqArAstANANtsArAps, and ANANANpqArAstANANrpAtAsp (used originally by  C. A. Meredith as single axioms for a related system) will do the job.

QUESTION C (page 106).
Is there a single axiom for classical logic in 'K' and 'N' using substitution and the rule "
From NK
αNβ and α, infer β"?  (Any other "reasonable" K-N rule would be an acceptable alternative, of course.)

QUESTION D (page 106; due originally to Peterson).
Is XCB = EpEEEpqErqr / p
(((pq)(rq))r)
a single axiom (with rules substitution and E-detachment, "From Eαβ and α, infer β") for the classical equivalential calculus?

UPDATE: Question D has been answered:  XCB is a single axiom for classical equivalence.  See L. Wos, D. Ulrich, and B. Fitelson, XCB: The last of the shortest single axioms for the classical equivalential calculus, Bulletin of the Section of Logic (University of Ldź), vol. 29 (2003), pp. 131-136, and Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus, Journal of Automated Reasoning, vol. 28 (2002), pp. 107-124.
          The 25-step proof from XCB presented there was subsequently shortened to 24 steps by Mark Stickel. Working from Stickel's proof, Larry Wos, proof crunching with William McCune's automated reasoning program
OTTER, has now reduced it to 22 steps.

QUESTION E (page 109).
Understanding a formula to be NN-free just in case no two negation signs occur consecutively in it, under what general conditions is it possible to construct an NN-free axiom set for a sentential system in which every NN-free theorem has an NN-free proof?

QUESTION F (page 109).
For those logics where it is possible to construct an axiom set of the sort described in Question E, what are some examples of such axiom sets?

QUESTION G (page 109).
Is there, in particular, an NN-free axiom set for classical logic in C and N in which every NN-free theorem has an NN-free proof?

UPDATE: Question G has been answered.  M. Beeson, R. Veroff, and L. Wos have shown [Double negation elimination in some propositional logics, Studia Logica, vol. 80 (2005), pp. 195-234]  that virtually all of the NN-free axiom sets for classical logic known in the literature (excluding only my pathological example developed on pp. 109-110 of the Legacy paper) permit NN-free proofs of their NN-free theorems, and take some steps towards answering Questions E and F above for the case of classical logic as well, and for the intuitionistic sentential calculus. 

QUESTION H (page 110).
Let Nn abbreviate the string consisting of n consecutive occurrences of 'N'. Under what general conditions is it possible to construct an Nn-free axiom set for a sentential system in which every Nn-free theorem has an Nn-free proof?

QUESTION I (page 110).
For those logics where it is possible to construct an axiom set of the sort described in Question H, what are some examples of such axiom sets?

QUESTION J (page 110).
Is there, in particular, an Nn-free axiom set for classical logic in C and N in which every Nn-free theorem has an Nn-free proof?

UPDATE: Presumably this question can be answered (affirmatively) with an easy modification of the methods used by Beeson, et al. to answer Question G.

QUESTION K (page 110).
Can one find metatheoretical results concerning the minimum variable complexity that can be attained in condensed detachment proofs from various axiom sets?

QUESTION L (page 111).
Is there an axiom set for full classical logic, or its implicational fragment, IF, or any other logic of interest for which there exists an "overhead" constant, c, such that for each positive integer n, each theorem involving at most n
distinct sentential letters has a condensed detachment proof in which no line involves more than n + c letters?

QUESTION M (page 112).
Are the formulas which have, over the years, been encountered often enough or been deemed important enough to acquire "nicknames" of their own--Id, Syl, Simp, Syl-Simp, Pon, Com, Syl*, etc. [thirty-two such formulas are listed on pages 103-104 of the Legacy paper] especially effective as resonators, as hints, and/or in proof sketches when doing searches using McCune's automated reasoning program
OTTER?

QUESTION N (page 112).
Can a fully-automated proof of the sufficiency of Meredith's 21-character single axiom,  CCCCCpqCNrNsrtCCtpCsp / ((((p
q)(~r~s))r)t)((tp)(sp)), for classical logic in C and N be found that equals (or shortens) Meredith's own derivation of Syl = CCpqCCqrCpr / ((pq)((qr)(pr)), Scotus = CpCNpq / p(~pq),  and Clavius = CCNppp / (~pp)p using just 41 condensed detachments?

UPDATE: Larry Wos has (with OTTER) now discovered a proof using only 38 applications of condensed detachment.  See Automated reasoning and the discovery of missing and elegant proofs, L. Wos and G. Peiper, Rinton, Paramus, 2003, sections 3.1 through 3.3.

 

QUESTION O (page 113; due originally to Prior).
Is there an independent pair of axioms for the implicational fragment IF of classical logic in which one member contains exactly 8 occurrences of C and the other is Cpp?

UPDATE: This question, a paraphrased version of Prior's original statement of it, should probably be revised to read "Is there an independent pair of organic axioms for...".  Otherwise, note that a trivial answer is provided by the pair {CCttCCCpqrCCrpCsp, Cpp}.  The two are independent, each giving (with substitution and detachment) only its own substitution instances, but Łukasiewicz's single axiom CCCpqrCCrpCsp for IF follows in a single step. (These same remarks apply also when Ctt is replaced in the first axiom by Cpp, Cqq, Crr, or Css.)
         
For the question thus revised, I have now found several solutions, for example, {CCCpqrCCCqstCCtqr, Cpp}.  The longer axiom therein is of course independent of Cpp since the latter alone gives only its own substitution instances. That Cpp is, in turn, independent of CCCpqrCCCqstCCtqr is shown by the matrix

                      
which was discovered by Meredith and used by him for a related purpose [in C.A. Meredith and A.N. Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, vol. IV (1963), pp. 171-187]. 
Łukasiewicz's single axiom again follows in a single step.
          Additional solutions include at least the pairs consisting of Cpp together with any one of CCpqCCCprsCCsqCtq, CCpqCCCqrsCCspCtq, CCpqCCCrspCCrpCtq, and CCpqCCCrsqCCrpCtq, though these develop more slowly.


QUESTION P
(page 113; due originally to Meredith).
Are Meredith's two 19-character single axioms for classical logic in C and the constant false operator 0 shortest possible?  Note that an affirmative answer would confirm Prior's conjecture that classical logic in C and 0 provides a simple example of a logic whose shortest axiomatization, measured by total symbol count, involves two axioms rather than just one, since the pair consisting of C0p together with
Łukasiewicz's single axiom CCCpqrCCrpCsp / ((pq)r)((rp)(s.p)) for classical implication is known to be a sufficient basis and contains just 16 symbols in all. 

UPDATE:  Z. Ernst, K. Harris, and B. Fitelson reported having shown that Meredith's two 19-symbol axioms are indeed shortest possible at AWARD 2001, the second annual Argonne Workshop on Automated Reasoning and Deduction, July 13-14, 2001, thus answering Question P affirmatively and consequently confirming Prior's conjecture. 

QUESTION Q (page 113; due originally to Prior).
Is Meredith's 19-character single axiom for classical logic in C and the constant true operator 1 shortest possible? (An affirmative answer would confirm another conjecture of Prior's that classical logic in C and 1 provides an example of a logic whose shortest axiomatization involves two axioms rather than one, since a shorter total axiomatization would then be given by the 16-symbol pair {
Łukasiewicz, Cp1} = {CCCpqrCCrpCsp, Cp1}).

QUESTION R (page 113; cf. Anderson and Belnap).
Is there a single axiom of somewhat reasonable length for the implicational fragment of Anderson and Belnap's system E of entailment? 

QUESTION S (page 113; cf. Anderson and Belnap).
Is there a single axiom of somewhat reasonable length for the implicational fragment of Anderson and Belnap's system R of relevant implication?  [The methods of A. Rezus, On a theorem of Tarski, Libertas Mathematica, vol. 2 (1982), pp. 63-97, answer Anderson and Belnap's original questions asking simply if single axioms for the implicational fragments of  E and R exist at all, but the axioms those methods produce are quite long. The questions remaining concern the existence of "short-ish" such axioms.]

UPDATE: There exists a 35-symbol 8-variable single axiom for implicational R.  For details, see the page for C-pure R.
 

QUESTION T (page 113).
Is there a single axiom of somewhat reasonable length for the C-pure fragment of any of the other standard systems in the Relevance Logic family?  (R. K. Meyer would especially like to know if a single axiom of any length exists for C-pure R-Mingle.)

UPDATE: D. Ulrich [On the existence of a single axiom for implicational R-mingle, abstract, Bulletin of Symbolic Logic, vol. 11 (2005), p 459], building on work of Ernst, Fitelson, Harris, and Wos, presents an 85-symbol 21-variable single axiom for R-Mingle.  I later improved it slightly to a 77-symbol single axiom containing occurrences of 19 distinct variables, and now have a 37-symbol axiom with 8 variables. Implicational R-Mingle has its own page elsewhere on this site and the <37, 8> axiom is shown there.
 

QUESTION U (page 114).
Does there exist a single axiom of reasonable length for classical logic with Sheffer's joint-denial operator S (sic) as sole connective?

UPDATE: Though I am not aware of any progress made to date on Question U,  B. Fitelson, K. Harris, and Z. Ernst have done extensive work on the similar question concerning the Sheffer stroke, D (sic), with the rule "From DαDβγ and α, infer γ".  Fitelson and Harris found more than sixty new single axioms of length 23, e.g., DDpDqrDDpDqrDDsrDDrsDps, to go along with the four single axioms of this length known previously from the work of Nicod, Łukasiewicz, and Wajsberg.  With Z. Ernst, they report having shown (by exhaustive search ruling out all shorter possibilities) that 23-symbol single axioms are shortest possible. 
     And does anyone know, by the way, how it came to be that standard Polish notation uses 'D' for the Sheffer stroke and 'S' for the daggar?   

QUESTION V (pages 114-116).
Are Meredith's two 17-symbol single axioms CCCpqrCsCCqCrtCqt and CpCCqrCCCsqCrtCqt for the implicational fragment HI of Heyting's intuitionistic sentential calculus shortest possible?  To complete the proof that they are, it suffices to show that none of the following four formulas are single axioms for HI:
                  C1.
CCCpqrCCqCrsCqs        C2. CCCpqrCCrCrsCqs       
                  C3. CCpCqrCCCspqCpr           C4.
CCpqCCCrpCqsCps

QUESTION W (page 116; due originally to Meredith).
Is there a 17-symbol single axiom for HI in which fewer than five distinct sentence letters occur?

QUESTION X (page 117; cf. Thomas).
What axiom sets exist for sentential logics besides IF in which most of the important and familiar theses can be obtained at very low proof levels?

QUESTION Y (page 117; cf. footnote 11).
What axiom sets exist for sentential logics besides HI, IF, and full classical logic in C and N in which most of the important and familiar theses can be obtained with the intrusion of few or no additional theorems as intermediate steps?

QUESTION Z (page 118).
For what familiar axiom sets can one or more of the axioms be replaced with its associated rule (as it is shown in the Legacy paper that CpCqp can be replaced in the two-base {CpCqp, CCpqCCpCqrCpr} for HI with the rule "From p, infer Cqp").

And a "bonus" question, QUESTION Z' (page 119):  In performing automated proof searches for systems with multiple axioms, is the strategy of instructing the program to choose from among the axioms, at each successive run, one to be employed only as major premise and never as minor sometimes useful?


Dolph Ulrich, 2007


 Entrance page | Home page | Twenty-six open questions |

Single axioms for:  | BCI | 4 subsystems of BCI | monothetic BCI | C-pure R | C-pure R-Mingle | C-pure LNo |
   
| BCK | C-pure intuitionism | Classical equivalence | A few more systems |

| D-complete axioms for (classical) equivalence | Exit page |