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)⊃((t⊃p)⊃(s⊃p)) for classical two-valued 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 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).
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. 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. 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. 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). 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 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).
QUESTION S
(page 113; cf. Anderson and Belnap).
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).
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).
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.
QUESTION V (pages 114-116). 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 | Twenty-six open questions | Single axioms for:
|
BCI |
4 subsystems of BCI |
monothetic BCI |
C-pure R |
C-pure R-Mingle |
C-pure
LNo | | D-complete axioms for (classical) equivalence | Exit page | |