The equivalential fragment EQ of
classical logic was first axiomatized by Leśniewski, using substitution
and E-detachment ("From Eαβ
and α,
infer β")
as rules together with the axioms EEEpqErpEqr / ((p≡q)≡(r≡p))≡(q≡r)
and EEpEqrEEpqr / (p≡(q≡r))≡((p≡q)≡r).
One of the most useful alternate two-bases found since is the pair {EEpqEEqrEpr,
EEpqEqp}, that is, {(p≡q)≡((q≡r)≡(p≡r)),
(p≡q)≡(q≡p)}.
The first single axioms for EQ were discovered by Wajsberg (EEEpEqrEErssEpq and EEEEpqrsEsEpEqr, each 15 symbols in length). Łukasiewicz then found three single axioms of length 11, and proved that they were shortest possible using six distinct matrices [there is an alternative proof, using a single matrix, in D. Ulrich, A five-valued model of the E-p-q theses, Notre Dame Journal of Formal Logic, vol. 29 (1988), pp. 137-138]. C. A. Meredith found seven additional axioms of length 11, and J. A. Kalman another (though he presents it as simply correcting a typographical error in an eighth one reported by Meredith). Winker found two more, and the 14th was found by Wos, Ulrich, and Fitelson as reported in the UPDATE to Question D on the Twenty-six open questions page. I note that the following list of single axioms for EQ of length 11 is complete, all other theorems of EQ of this length having been ruled out earlier, most by J. G. Peterson [The possible shortest single axioms for EC-tautologies, Report No. 105, University of Auckland, Department of Mathematics] and the rest by Wos et. al [Questions concerning possible shortest single axioms for the equivalential calculus: An application of automated theorem proving in infinite domains, Notre Dame Journal of Formal Logic, vol. 24 (1983), pp. 205-223]. The names used below for EQ theorems of length 11 follow the conventions worked out by J. A. Kalman and have now become standard. Click here for a detailed account of those conventions.
EEpqEErqEpr / (p≡q)≡[(r≡q)≡(p≡r)]
(YQL)
EEEpqrEqErp / [(p≡q)≡r]≡[q≡(r≡p)]
(UM) |
||
OPEN QUESTIONS Is BXO = EEEEpEqrrqp / [{[p≡(q≡r)]≡r}≡q]≡p a single axiom for EQ when both detachment and reverse detachment are rules? Is XMO = EpEqErEErqp / p≡[q≡{r≡[(r≡q)≡p]}] a single axiom for EQ when both detachment and reverse detachment are rules? Is AXL = EEEEEpqrqpr / [{[(p≡q)≡r]≡q}≡p]≡r a single axiom for EQ when both detachment and reverse detachment are rules? UPDATE: Despite Hodgson's remark that any matrix showing that AXL is not a single axiom must contain at least seven values, I showed (at AWARD 2004) that the following six-valued matrix does the job by validating AXL as well as both rules but rejecting the EQ theorem EEpqEEqrEpr / (p≡q)≡((q≡r)≡(p≡r)):
E | 1 2 3
4 5 6
. UPDATE: Similarly, I showed that XNK is not a single axiom via the matrix
Is XBC
= EpEEEpEqrrq / p≡[{[p≡(q≡r)]≡r
}≡q]
a single axiom for EQ when both detachment and reverse detachment are
rules? |
||
© 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 | | D-complete axioms for (classical) equivalence | Exit page | |