Listed below are the twentysix 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. 97122].
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 email me updated 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 21character single axiom CCCCCpqCNrNsrtCCtpCsp / ((((p⊃q)⊃(~r⊃~s))⊃r)⊃t)⊃((t⊃p)⊃(s⊃p)) for classical twovalued logic using the standard connectives 'C' and 'N' shortest possible?
QUESTION B (page 106). UPDATE: Question B has been answered by Willemien Hoogendoorn of Birkbeck College, London, UK, via email. 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).
QUESTION D
(page 106; due originally to Peterson).
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 Lódź),
vol. 29
(2003), pp. 131136,
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. 107124. QUESTION
E
(page 109). QUESTION F
(page 109). QUESTION G
(page 109). 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. 195234] that virtually all of the NNfree axiom sets for classical logic known in the literature (excluding only my pathological example developed on pp. 109110 of the Legacy paper) permit NNfree proofs of their NNfree 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). QUESTION I
(page 110). QUESTION J
(page 110). 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). QUESTION L
(page 111). QUESTION M
(page 112). QUESTION N
(page 112). 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).
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.)
UPDATE: Z. Ernst, K. Harris, and B. Fitelson reported having shown that Meredith's two 19symbol axioms are indeed shortest possible at AWARD 2001, the second annual Argonne Workshop on Automated Reasoning and Deduction, July 1314, 2001, thus answering Question P affirmatively and consequently confirming Prior's conjecture. QUESTION Q
(page 113; due originally
to Prior).
QUESTION S
(page 113; cf. Anderson and Belnap).
UPDATE:
There exists a 35symbol 8variable single axiom for implicational R. For
details, see the page for Cpure R. QUESTION T
(page 113).
UPDATE:
D. Ulrich [On the existence of a single axiom
for implicational Rmingle, abstract, Bulletin of Symbolic Logic,
vol. 11 (2005), p 459], building on work of
Ernst, Fitelson, Harris, and Wos,
presents an 85symbol 21variable single axiom for RMingle.
I later improved it slightly to a 77symbol single axiom containing occurrences
of 19 distinct variables, and now have a 37symbol axiom with 8 variables.
Implicational RMingle has
its own page elsewhere on
this site and the <37, 8> axiom is shown there. QUESTION U
(page 114).
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 23symbol single axioms are
shortest possible.
QUESTION V (pages 114116). QUESTION W
(page 116; due originally to Meredith). QUESTION X
(page 117; cf. Thomas). QUESTION Y
(page 117; cf. footnote 11). QUESTION Z
(page 118). 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? 

Entrance page  Home page  Twentysix open questions  Single axioms for:

BCI 
4 subsystems of BCI 
monothetic BCI 
Cpure R 
Cpure RMingle 
Cpure
LNo   Dcomplete axioms for (classical) equivalence  Exit page  