|
Kalman's naming conventions for the length-11 EQ theses The following conventions for "naming"
each of the 630 length-11 theorems of the classical equivalential calculus
EQ first appeared in J. G. Peterson's The possible shortest
single axioms for EC-tautologies, Report No. 105, University of
Auckland, Department of Mathematics. They were later published as Appendix
1 of Kahlil Hodgson's Shortest single axioms for the equivalential
calculus with CD and RCD, Journal of Automated Reasoning,
vol. 20 (1998), pp. 283-316, where it is made clear that they are due to
J. A. Kalman. |
|||||
| T = EEExxxEExxx | U = EEExxxExExx | V = EExExxEExxx | W = EExExxExExx | ||
Otherwise, α and β are of different lengths. In that case, each of them must be of one of the following forms and the bracket-type of Eαβ is coded by the letter coding the bracket-type of α followed by the letter coding the bracket-type of β: |
|||||
|
A = EEEExxxxx B = EEExExxxx C = EEExxExxx D = EEExxxExx E = EExEExxxx F = EExExExxx G = EExExxExx H = EExxEExxx I = EExxExExx J = ExEEExxxx K = ExEExExxx L = ExEExxExx M = ExExEExxx N = ExExExExx |
O = EEExxxx P = EExExxx Q = EExxExx R = ExEExxx S = ExExExx |
Y = Exx | X = x | ||
Each 11-symbol theorem of EQ contains two occurrences of p, two of q, and two of r. Up to alphabetical variance, there are 15 orders in which these may occur. The full name for the theorem in question is then given by following the code letter(s) for its bracket-type with the code letter for the order in which the sentential variables appear in it: |
|||||
|
A = ppqqrr D = pqpqrr G = pqqprr J = pqrpqr M = pqrqrp |
B = ppqrqr E = pqprqr H = pqqrpr K = pqrprq N = pqrrpq |
C = ppqrrq F = pqprrq I = pqqrrp L = pqrqpr O = pqrrqp |
|||
|
ILLUSTRATION 1. What is the name of the formula EEEpEqrrEqp? ANSWER. It is of the form EEExExxxExx, and the letters in it occur in the order pqrrqp. Since EExExxx is of bracket-type P, Exx is of bracket-type Y, and pqrrqp is letter-order O, its name is PYO. ILLUSTRATION 2. What is the formula whose name is YQJ? ANSWER. It's left-most part has bracket-type Y = Exx and its right-most part has bracket-type Q = EExxExx, so it itself has bracket-type EYQ = EExxEExxExx. The sentential letters occurring in it occur in the order J = pqrpqr. So YQJ is the formula EEpqEErpEqr. |
|||||
|
THE 630 EQ THESES OF LENGTH
ELEVEN vertical space |
||||
|
AXA. EEEEEppqqrr AXD. EEEEEpqpqrr AXG. EEEEEpqqprr AXJ. EEEEEpqrpqr AXM. EEEEEpqrqrp BXA. EEEEpEpqqrr BXD. EEEEpEqpqrr BXG. EEEEpEqqprr BXJ. EEEEpEqrpqr BXM. EEEEpEqrqrp CXA. EEEEppEqqrr CXD. EEEEpqEpqrr CXG. EEEEpqEqprr CXJ. EEEEpqErpqr CXM. EEEEpqErqrp DXA. EEEEppqEqrr DXD. EEEEpqpEqrr DXG. EEEEpqqEprr DXJ. EEEEpqrEpqr DXM. EEEEpqrEqrp OYA. EEEEppqqErr OYD. EEEEpqpqErr OYG. EEEEpqqpErr OYJ. EEEEpqrpEqr OYM. EEEEpqrqErp EXA. EEEpEEpqqrr EXD. EEEpEEqpqrr EXG. EEEpEEqqprr EXJ. EEEpEEqrpqr EXM. EEEpEEqrqrp FXA. EEEpEpEqqrr FXD. EEEpEqEpqrr FXG. EEEpEqEqprr FXJ. EEEpEqErpqr FXM. EEEpEqErqrp GXA. EEEpEpqEqrr GXD. EEEpEqpEqrr GXG. EEEpEqqEprr GXJ. EEEpEqrEpqr GXM. EEEpEqrEqrp PYA. EEEpEpqqErr PYD. EEEpEqpqErr PYG. EEEpEqqpErr PYJ. EEEpEqrpEqr PYM. EEEpEqrqErp HXA. EEEppEEqqrr HXD. EEEpqEEpqrr HXG. EEEpqEEqprr HXJ. EEEpqEErpqr HXM. EEEpqEErqrp IXA. EEEppEqEqrr IXD. EEEpqEpEqrr IXG. EEEpqEqEprr IXJ. EEEpqErEpqr IXM. EEEpqErEqrp QYA. EEEppEqqErr QYD. EEEpqEpqErr QYG. EEEpqEqpErr QYJ. EEEpqErpEqr QYM. EEEpqErqErp TA. EEEppqEEqrr TD. EEEpqpEEqrr TG. EEEpqqEEprr TJ. EEEpqrEEpqr TM. EEEpqrEEqrp UA. EEEppqEqErr UD. EEEpqpEqErr UG. EEEpqqEpErr UJ. EEEpqrEpEqr UM. EEEpqrEqErp JXA. EEpEEEpqqrr JXD. EEpEEEqpqrr JXG. EEpEEEqqprr JXJ. EEpEEEqrpqr JXM. EEpEEEqrqrp KXA. EEpEEpEqqrr KXD. EEpEEqEpqrr KXG. EEpEEqEqprr KXJ. EEpEEqErpqr KXM. EEpEEqErqrp LXA. EEpEEpqEqrr LXD. EEpEEqpEqrr LXG. EEpEEqqEprr LXJ. EEpEEqrEpqr LXM. EEpEEqrEqrp RYA. EEpEEpqqErr RYD. EEpEEqpqErr RYG. EEpEEqqpErr RYJ. EEpEEqrpEqr RYM. EEpEEqrqErp MXA. EEpEpEEqqrr MXD. EEpEqEEpqrr MXG. EEpEqEEqprr MXJ. EEpEqEErpqr MXM. EEpEqEErqrp NXA. EEpEpEqEqrr NXD. EEpEqEpEqrr NXG. EEpEqEqEprr NXJ. EEpEqErEpqr NXM. EEpEqErEqrp SYA. EEpEpEqqErr SYD. EEpEqEpqErr SYG. EEpEqEqpErr SYJ. EEpEqErpEqr SYM. EEpEqErqErp VA. EEpEpqEEqrr VD. EEpEqpEEqrr VG. EEpEqqEEprr VJ. EEpEqrEEpqr VM. EEpEqrEEqrp WA. EEpEpqEqErr WD. EEpEqpEqErr WG. EEpEqqEpErr WJ. EEpEqrEpEqr WM. EEpEqrEqErp YOA. EEppEEEqqrr YOD. EEpqEEEpqrr YOG. EEpqEEEqprr YOJ. EEpqEEErpqr YOM. EEpqEEErqrp YPA. EEppEEqEqrr YPD. EEpqEEpEqrr YPG. EEpqEEqEprr YPJ. EEpqEErEpqr YPM. EEpqEErEqrp YQA. EEppEEqqErr YQD. EEpqEEpqErr YQG. EEpqEEqpErr YQJ. EEpqEErpEqr YQM. EEpqEErqErp YRA. EEppEqEEqrr YRD. EEpqEpEEqrr YRG. EEpqEqEEprr YRJ. EEpqErEEpqr YRM. EEpqErEEqrp YSA. EEppEqEqErr YSD. EEpqEpEqErr YSG. EEpqEqEpErr YSJ. EEpqErEpEqr YSM. EEpqErEqErp XAA. EpEEEEpqqrr XAD. EpEEEEqpqrr XAG. EpEEEEqqprr XAJ. EpEEEEqrpqr XAM. EpEEEEqrqrp XBA. EpEEEpEqqrr XBD. EpEEEqEpqrr XBG. EpEEEqEqprr XBJ. EpEEEqErpqr XBM. EpEEEqErqrp XCA. EpEEEpqEqrr XCD. EpEEEqpEqrr XCG. EpEEEqqEprr XCJ. EpEEEqrEpqr XCM. EpEEEqrEqrp XDA. EpEEEpqqErr XDD. EpEEEqpqErr XDG. EpEEEqqpErr XDJ. EpEEEqrpEqr XDM. EpEEEqrqErp XEA. EpEEpEEqqrr XED. EpEEqEEpqrr XEG. EpEEqEEqprr XEJ. EpEEqEErpqr XEM. EpEEqEErqrp XFA. EpEEpEqEqrr XFD. EpEEqEpEqrr XFG. EpEEqEqEprr XFJ. EpEEqErEpqr XFM. EpEEqErEqrp XGA. EpEEpEqqErr XGD. EpEEqEpqErr XGG. EpEEqEqpErr XGJ. EpEEqErpEqr XGM. EpEEqErqErp XHA. EpEEpqEEqrr XHD. EpEEqpEEqrr XHG. EpEEqqEEprr XHJ. EpEEqrEEpqr XHM. EpEEqrEEqrp XIA. EpEEpqEqErr XID. EpEEqpEqErr XIG. EpEEqqEpErr XIJ. EpEEqrEpEqr XIM. EpEEqrEqErp XJA. EpEpEEEqqrr XJD. EpEqEEEpqrr XJG. EpEqEEEqprr XJJ. EpEqEEErpqr XJM. EpEqEEErqrp XKA. EpEpEEqEqrr XKD. EpEqEEpEqrr XKG. EpEqEEqEprr XKJ. EpEqEErEpqr XKM. EpEqEErEqrp XLA. EpEpEEqqErr XLD. EpEqEEpqErr XLG. EpEqEEqpErr XLJ. EpEqEErpEqr XLM. EpEqEErqErp XMA. EpEpEqEEqrr XMD. EpEqEpEEqrr XMG. EpEqEqEEprr XMJ. EpEqErEEpqr XMM. EpEqErEEqrp XNA. EpEpEqEqErr XND. EpEqEpEqErr XNG. EpEqEqEpErr XNJ. EpEqErEpEqr XNM. EpEqErEqErp |
AXB. EEEEEppqrqr AXE. EEEEEpqprqr AXH. EEEEEpqqrpr AXK. EEEEEpqrprq AXN. EEEEEpqrrpq BXB. EEEEpEpqrqr BXE. EEEEpEqprqr BXH. EEEEpEqqrpr BXK. EEEEpEqrprq BXN. EEEEpEqrrpq CXB. EEEEppEqrqr CXE. EEEEpqEprqr CXH. EEEEpqEqrpr CXK. EEEEpqErprq CXN. EEEEpqErrpq DXB. EEEEppqErqr DXE. EEEEpqpErqr DXH. EEEEpqqErpr DXK. EEEEpqrEprq DXN. EEEEpqrErpq OYB. EEEEppqrEqr OYE. EEEEpqprEqr OYH. EEEEpqqrEpr OYK. EEEEpqrpErq OYN. EEEEpqrrEpq EXB. EEEpEEpqrqr EXE. EEEpEEqprqr EXH. EEEpEEqqrpr EXK. EEEpEEqrprq EXN. EEEpEEqrrpq FXB. EEEpEpEqrqr FXE. EEEpEqEprqr FXH. EEEpEqEqrpr FXK. EEEpEqErprq FXN. EEEpEqErrpq GXB. EEEpEpqErqr GXE. EEEpEqpErqr GXH. EEEpEqqErpr GXK. EEEpEqrEprq GXN. EEEpEqrErpq PYB. EEEpEpqrEqr PYE. EEEpEqprEqr PYH. EEEpEqqrEpr PYK. EEEpEqrpErq PYN. EEEpEqrrEpq HXB. EEEppEEqrqr HXE. EEEpqEEprqr HXH. EEEpqEEqrpr HXK. EEEpqEErprq HXN. EEEpqEErrpq IXB. EEEppEqErqr IXE. EEEpqEpErqr IXH. EEEpqEqErpr IXK. EEEpqErEprq IXN. EEEpqErErpq QYB. EEEppEqrEqr QYE. EEEpqEprEqr QYH. EEEpqEqrEpr QYK. EEEpqErpErq QYN. EEEpqErrEpq TB. EEEppqEErqr TE. EEEpqpEErqr TH. EEEpqqEErpr TK. EEEpqrEEprq TN. EEEpqrEErpq UB. EEEppqErEqr UE. EEEpqpErEqr UH. EEEpqqErEpr UK. EEEpqrEpErq UN. EEEpqrErEpq JXB. EEpEEEpqrqr JXE. EEpEEEqprqr JXH. EEpEEEqqrpr JXK. EEpEEEqrprq JXN. EEpEEEqrrpq KXB. EEpEEpEqrqr KXE. EEpEEqEprqr KXH. EEpEEqEqrpr KXK. EEpEEqErprq KXN. EEpEEqErrpq LXB. EEpEEpqErqr LXE. EEpEEqpErqr LXH. EEpEEqqErpr LXK. EEpEEqrEprq LXN. EEpEEqrErpq RYB. EEpEEpqrEqr RYE. EEpEEqprEqr RYH. EEpEEqqrEpr RYK. EEpEEqrpErq RYN. EEpEEqrrEpq MXB. EEpEpEEqrqr MXE. EEpEqEEprqr MXH. EEpEqEEqrpr MXK. EEpEqEErprq MXN. EEpEqEErrpq NXB. EEpEpEqErqr NXE. EEpEqEpErqr NXH. EEpEqEqErpr NXK. EEpEqErEprq NXN. EEpEqErErpq SYB. EEpEpEqrEqr SYE. EEpEqEprEqr SYH. EEpEqEqrEpr SYK. EEpEqErpErq SYN. EEpEqErrEpq VB. EEpEpqEErqr VE. EEpEqpEErqr VH. EEpEqqEErpr VK. EEpEqrEEprq VN. EEpEqrEErpq WB. EEpEpqErEqr WE. EEpEqpErEqr WH. EEpEqqErEpr WK. EEpEqrEpErq WN. EEpEqrErEpq YOB. EEppEEEqrqr YOE. EEpqEEEprqr YOH. EEpqEEEqrpr YOK. EEpqEEErprq YON. EEpqEEErrpq YPB. EEppEEqErqr YPE. EEpqEEpErqr YPH. EEpqEEqErpr YPK. EEpqEErEprq YPN. EEpqEErErpq YQB. EEppEEqrEqr YQE. EEpqEEprEqr YQH. EEpqEEqrEpr YQK. EEpqEErpErq YQN. EEpqEErrEpq YRB. EEppEqEErqr YRE. EEpqEpEErqr YRH. EEpqEqEErpr YRK. EEpqErEEprq YRN. EEpqErEErpq YSB. EEppEqErEqr YSE. EEpqEpErEqr YSH. EEpqEqErEpr YSK. EEpqErEpErq YSN. EEpqErErEpq XAB. EpEEEEpqrqr XAE. EpEEEEqprqr XAH. EpEEEEqqrpr XAK. EpEEEEqrprq XAN. EpEEEEqrrpq XBB. EpEEEpEqrqr XBE. EpEEEqEprqr XBH. EpEEEqEqrpr XBK. EpEEEqErprq XBN. EpEEEqErrpq XCB. EpEEEpqErqr XCE. EpEEEqpErqr XCH. EpEEEqqErpr XCK. EpEEEqrEprq XCN. EpEEEqrErpq XDB. EpEEEpqrEqr XDE. EpEEEqprEqr XDH. EpEEEqqrEpr XDK. EpEEEqrpErq XDN. EpEEEqrrEpq XEB. EpEEpEEqrqr XEE. EpEEqEEprqr XEH. EpEEqEEqrpr XEK. EpEEqEErprq XEN. EpEEqEErrpq XFB. EpEEpEqErqr XFE. EpEEqEpErqr XFH. EpEEqEqErpr XFK. EpEEqErEprq XFN. EpEEqErErpq XGB. EpEEpEqrEqr XGE. EpEEqEprEqr XGH. EpEEqEqrEpr XGK. EpEEqErpErq XGN. EpEEqErrEpq XHB. EpEEpqEErqr XHE. EpEEqpEErqr XHH. EpEEqqEErpr XHK. EpEEqrEEprq XHN. EpEEqrEErpq XIB. EpEEpqErEqr XIE. EpEEqpErEqr XIH. EpEEqqErEpr XIK. EpEEqrEpErq XIN. EpEEqrErEpq XJB. EpEpEEEqrqr XJE. EpEqEEEprqr XJH. EpEqEEEqrpr XJK. EpEqEEErprq XJN. EpEqEEErrpq XKB. EpEpEEqErqr XKE. EpEqEEpErqr XKH. EpEqEEqErpr XKK. EpEqEErEprq XKN. EpEqEErErpq XLB. EpEpEEqrEqr XLE. EpEqEEprEqr XLH. EpEqEEqrEpr XLK. EpEqEErpErq XLN. EpEqEErrEpq XMB. EpEpEqEErqr XME. EpEqEpEErqr XMH. EpEqEqEErpr XMK. EpEqErEEprq XMN. EpEqErEErpq XNB. EpEpEqErEqr XNE. EpEqEpErEqr XNH. EpEqEqErEpr XNK. EpEqErEpErq XNN. EpEqErErEpq |
AXC.
EEEEEppqrrq AXF. EEEEEpqprrq AXI. EEEEEpqqrrp AXL. EEEEEpqrqpr AXO. EEEEEpqrrqp BXC. EEEEpEpqrrq BXF. EEEEpEqprrq BXI. EEEEpEqqrrp BXL. EEEEpEqrqpr BXO. EEEEpEqrrqp CXC. EEEEppEqrrq CXF. EEEEpqEprrq CXI. EEEEpqEqrrp CXL. EEEEpqErqpr CXO. EEEEpqErrqp DXC. EEEEppqErrq DXF. EEEEpqpErrq DXI. EEEEpqqErrp DXL. EEEEpqrEqpr DXO. EEEEpqrErqp OYC. EEEEppqrErq OYF. EEEEpqprErq OYI. EEEEpqqrErp OYL. EEEEpqrqEpr OYO. EEEEpqrrEqp EXC. EEEpEEpqrrq EXF. EEEpEEqprrq EXI. EEEpEEqqrrp EXL. EEEpEEqrqpr EXO. EEEpEEqrrqp FXC. EEEpEpEqrrq FXF. EEEpEqEprrq FXI. EEEpEqEqrrp FXL. EEEpEqErqpr FXO. EEEpEqErrqp GXC. EEEpEpqErrq GXF. EEEpEqpErrq GXI. EEEpEqqErrp GXL. EEEpEqrEqpr GXO. EEEpEqrErqp PYC. EEEpEpqrErq PYF. EEEpEqprErq PYI. EEEpEqqrErp PYL. EEEpEqrqEpr PYO. EEEpEqrrEqp HXC. EEEppEEqrrq HXF. EEEpqEEprrq HXI. EEEpqEEqrrp HXL. EEEpqEErqpr HXO. EEEpqEErrqp IXC. EEEppEqErrq IXF. EEEpqEpErrq IXI. EEEpqEqErrp IXL. EEEpqErEqpr IXO. EEEpqErErqp QYC. EEEppEqrErq QYF. EEEpqEprErq QYI. EEEpqEqrErp QYL. EEEpqErqEpr QYO. EEEpqErrEqp TC. EEEppqEErrq TF. EEEpqpEErrq TI. EEEpqqEErrp TL. EEEpqrEEqpr TO. EEEpqrEErqp UC. EEEppqErErq UF. EEEpqpErErq UI. EEEpqqErErp UL. EEEpqrEqEpr UO. EEEpqrErEqp JXC. EEpEEEpqrrq JXF. EEpEEEqprrq JXI. EEpEEEqqrrp JXL. EEpEEEqrqpr JXO. EEpEEEqrrqp KXC. EEpEEpEqrrq KXF. EEpEEqEprrq KXI. EEpEEqEqrrp KXL. EEpEEqErqpr KXO. EEpEEqErrqp LXC. EEpEEpqErrq LXF. EEpEEqpErrq LXI. EEpEEqqErrp LXL. EEpEEqrEqpr LXO. EEpEEqrErqp RYC. EEpEEpqrErq RYF. EEpEEqprErq RYI. EEpEEqqrErp RYL. EEpEEqrqEpr RYO. EEpEEqrrEqp MXC. EEpEpEEqrrq MXF. EEpEqEEprrq MXI. EEpEqEEqrrp MXL. EEpEqEErqpr MXO. EEpEqEErrqp NXC. EEpEpEqErrq NXF. EEpEqEpErrq NXI. EEpEqEqErrp NXL. EEpEqErEqpr NXO. EEpEqErErqp SYC. EEpEpEqrErq SYF. EEpEqEprErq SYI. EEpEqEqrErp SYL. EEpEqErqEpr SYO. EEpEqErrEqp VC. EEpEpqEErrq VF. EEpEqpEErrq VI. EEpEqqEErrp VL. EEpEqrEEqpr VO. EEpEqrEErqp WC. EEpEpqErErq WF. EEpEqpErErq WI. EEpEqqErErp WL. EEpEqrEqEpr WO. EEpEqrErEqp YOC. EEppEEEqrrq YOF. EEpqEEEprrq YOI. EEpqEEEqrrp YOL. EEpqEEErqpr YOO. EEpqEEErrqp YPC. EEppEEqErrq YPF. EEpqEEpErrq YPI. EEpqEEqErrp YPL. EEpqEErEqpr YPO. EEpqEErErqp YQC. EEppEEqrErq YQF. EEpqEEprErq YQI. EEpqEEqrErp YQL. EEpqEErqEpr YQO. EEpqEErrEqp YRC. EEppEqEErrq YRF. EEpqEpEErrq YRI. EEpqEqEErrp YRL. EEpqErEEqpr YRO. EEpqErEErqp YSC. EEppEqErErq YSF. EEpqEpErErq YSI. EEpqEqErErp YSL. EEpqErEqEpr YSO. EEpqErErEqp XAC. EpEEEEpqrrq XAF. EpEEEEqprrq XAI. EpEEEEqqrrp XAL. EpEEEEqrqpr XAO. EpEEEEqrrqp XBC. EpEEEpEqrrq XBF. EpEEEqEprrq XBI. EpEEEqEqrrp XBL. EpEEEqErqpr XBO. EpEEEqErrqp XCC. EpEEEpqErrq XCF. EpEEEqpErrq XCI. EpEEEqqErrp XCL. EpEEEqrEqpr XCO. EpEEEqrErqp XDC. EpEEEpqrErq XDF. EpEEEqprErq XDI. EpEEEqqrErp XDL. EpEEEqrqEpr XDO. EpEEEqrrEqp XEC. EpEEpEEqrrq XEF. EpEEqEEprrq XEI. EpEEqEEqrrp XEL. EpEEqEErqpr XEO. EpEEqEErrqp XFC. EpEEpEqErrq XFF. EpEEqEpErrq XFI. EpEEqEqErrp XFL. EpEEqErEqpr XFO. EpEEqErErqp XGC. EpEEpEqrErq XGF. EpEEqEprErq XGI. EpEEqEqrErp XGL. EpEEqErqEpr XGO. EpEEqErrEqp XHC. EpEEpqEErrq XHF. EpEEqpEErrq XHI. EpEEqqEErrp XHL. EpEEqrEEqpr XHO. EpEEqrEErqp XIC. EpEEpqErErq XIF. EpEEqpErErq XII. EpEEqqErErp XIL. EpEEqrEqEpr XIO. EpEEqrErEqp XJC. EpEpEEEqrrq XJF. EpEqEEEprrq XJI. EpEqEEEqrrp XJL. EpEqEEErqpr XJO. EpEqEEErrqp XKC. EpEpEEqErrq XKF. EpEqEEpErrq XKI. EpEqEEqErrp XKL. EpEqEErEqpr XKO. EpEqEErErqp XLC. EpEpEEqrErq XLF. EpEqEEprErq XLI. EpEqEEqrErp XLL. EpEqEErqEpr XLO. EpEqEErrEqp XMC. EpEpEqEErrq XMF. EpEqEpEErrq XMI. EpEqEqEErrp XML. EpEqErEEqpr XM0. EpEqErEErqp XNC. EpEpEqErErq XNF. EpEqEpErErq XNI. EpEqEqErErp XNL. EpEqErEqEpr XNO. EpEqErErEqp © Dolph Ulrich, 2007 |
||