# 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