Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus

Details Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus

2002-11-13

arxiv.org/abs/cs/0211014v1

Computer Science

Logic in Computer Science

21 pages, no figures

Scientific paper

With the inclusion of an effective methodology, this article answers in detail a question that, for a quarter of a century, remained open despite intense study by various researchers. Is the formula XCB = e(x,e(e(e(x,y),e(z,y)),z)) a single axiom for the classical equivalential calculus when the rules of inference consist of detachment (modus ponens) and substitution? Where the function e represents equivalence, this calculus can be axiomatized quite naturally with the formulas e(x,x), e(e(x,y),e(y,x)), and e(e(x,y),e(e(y,z),e(x,z))), which correspond to reflexivity, symmetry, and transitivity, respectively. (We note that e(x,x) is dependent on the other two axioms.) Heretofore, thirteen shortest single axioms for classical equivalence of length eleven had been discovered, and XCB was the only remaining formula of that length whose status was undetermined. To show that XCB is indeed such a single axiom, we focus on the rule of condensed detachment, a rule that captures detachment together with an appropriately general, but restricted, form of substitution. The proof we present in this paper consists of twenty-five applications of condensed detachment, completing with the deduction of transitivity followed by a deduction of symmetry. We also discuss some factors that may explain in part why XCB resisted relinquishing its treasure for so long. Our approach relied on diverse strategies applied by the automated reasoning program OTTER. Thus ends the search for shortest single axioms for the equivalential calculus.

Affiliated with

Also associated with

No associations

Rating

Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-293779