Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus
David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
With the inclusion of an e ective 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 (x x), e(e(x y) e(y x)), and e(e(x y) e(e(y z) e(x z))), which correspond to reexivity, 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- ve 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.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
T. Thacher Robinson (1968). Independence of Two Nice Sets of Axioms for the Propositional Calculus. Journal of Symbolic Logic 33 (2):265-270.
J. A. Kalman (1982). The Two-Property and Condensed Detachment. Studia Logica 41 (2-3):173 - 179.
Branden Fitelson & Larry Wos (2001). Finding Missing Proofs with Automated Reasoning. Studia Logica 68 (3):329-356.
L. Wos, S. Winker, R. Veroff, B. Smith & L. Henschen (1983). Questions Concerning Possible Shortest Single Axioms for the Equivalential Calculus: An Application of Automated Theorem Proving to Infinite Domains. Notre Dame Journal of Formal Logic 24 (2):205-223.
Dolph Ulrich (1996). The Shortest Possible Length of the Longest Implicational Axiom. Journal of Philosophical Logic 25 (1):101 - 108.
Jeremy George Peterson (1976). Shortest Single Axioms for the Classical Equivalential Calculus. Notre Dame Journal of Formal Logic 17 (2):267-271.
John A. Kalman (1978). A Shortest Single Axiom for the Classical Equivalential Calculus. Notre Dame Journal of Formal Logic 19 (1):141-144.
Zachary Ernst, Branden Fitelson, Kenneth Harris & Larry Wos (2002). Shortest Axiomatizations of Implicational S4 and S. Notre Dame Journal of Formal Logic 43 (3):169-179.
Branden Fitelson (2002). Shortest Axiomatizations of Implicational S4 and S5. Notre Dame Journal of Formal Logic 43 (3):169-179.
Added to index2009-01-28
Total downloads18 ( #194,551 of 1,790,294 )
Recent downloads (6 months)10 ( #83,505 of 1,790,294 )
How can I increase my downloads?