Single Axiom for Orthomodular Lattices

Back to the Main Page

Summary. We can eliminate all OML Sheffer stroke candidates up through length 19, we can eliminate all all but 58 candidates of length 21, and we present a single axiom of length 23.

Generating equations satisfying properties 1--7 is the same as in the OL case. However, for property 8, we do not have a decision procedure for OML identities. Therefore, we check against a small set of OMLs.

Up Through Length 19 (OML)

We can eliminate all candidates up through length 19 by using the OML of size 6 (interps/OML.6, see Table 1) for step 8, and a set of nine non-OMLs (interps/non-OL.B-9) for step 9. Note that the nine non-OMLs also happen to be non-OLs.

Note that in this case, any unsound candidates that slipped through step 8 are killed in step 9.

Length 21 (OML)

We cannot yet eliminate all candidates of length 21. If we use the OML of size 6 (interps/OML.6) and the two OMLs of size 10 (interps/OML.10) for step 8, and if we use a set of 23 non-OMLs (interps/non-OL.C-23 for step 9, we can eliminate all but 58 candidates.

We have not found proofs or countermodels for any of the 58 surviving candidates. Recall that the method we used to produce the 58 candidates does not necessarily produce OML identities, but we have used Otter to show that 40 of the 58 (enumerate/OML/21/sound/58-denials.out) are OML identities.

When we told Norm Megill about this work, he proved (by hand, using the Foulis-Holland theorem) that the remaining 18 OML candidates are, in fact, OML identities.

Length 23 (OML)

Applying the same method and filter to the 3 and 4 variable equations of length 23 yields 3053 candidates.

The script enumerate/OML/23/go does that and then sends those candidates to ploop3 which calls Otter for each candidate. Otter proved several of the 3053 candidates to be single axioms, including the following.

     f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x.  % OML-Sh

Recall that the method for OML does not necessarily produce OML identities, so we have to give a soundness proof as well as a completeness proof.

Completeness Proofs (OML)

Here are two completeness proofs. The first proves the Sheffer stroke OML 3-basis from OML-sax, and the second proves the join/complement 3-basis.

    otter < OML-Sh.in > OML-Sh.out
    otter < OML-Sh-jc.in > OML-Sh-jc.out

Soundness Proofs (OML)

We give two soundness proofs, that is, proofs that it is an OML identity. The first proves OML-sax from the Sheffer OML 3-basis, and the second proves it from the join/complement OML 5-basis.

    otter < OML-Sh-sound.in > OML-Sh-sound.out