# Single Axiom for Modular Ortholattices

Back to the Main Page
*Summary*. We can eliminate all candidates up through length 19,
and we can eliminate all but 238 candidates of length 21.
A single axiom of length 25 was found.

## Up Through Length 19 (MOL)

The exhaustive search showing that there is no OML single axiom
up through length 19 also shows that there is no MOL
single axiom up through length 19. Consider steps 8 and 9
of the OML case.
- Step 8 uses OML.6. However, OML.6 is also a MOL
so all MOL identities (and possibly some non-MOL identities)
pass step 8.
- Step 9 uses non-OL.B-9, which are non-MOLs.

Therefore, there is no Sheffer stroke single axiom for
MOL of length less than 21.
## Length 21 (MOL)

For the length 21 OML case, we used the two OMLs of size 10 for step 8.
However, one of those OMLs is not a MOL, so we cannot use it here.
If we run the same job as in the OML case, but with
the one MOL of size 10 instead of the two OMLs of size 10,
we get
331 candidates
instead of 58. (In fact, the MOL.10 does not help us.)
By using MACE to look for non-MOL models of those 331 candidates,
we found 14 models, which all turn out to be non-OLs
(interps/non-OL.D-14).
These reduce the number of candidates to
296.

Finally, by using the 9 OMLs that are not MOLs, up through size 16
(interps/non-MOL-OML)
(see Table 1), we can reduce the number of candidates to 238.

If there is a length-21 Sheffer stroke single axiom for MOL,
it is among these
238 candidates.
Although in general step 8 is unsound, in this case all of the candidates turn
out to be MOL identities
(enumerate/MOL/21/sound/238-denials.out)

## Lengths 23, 25, 27 (MOL)

For length 23, we generated and filtered all equations satisfying
properties 1-7 (which took a few days of computing), but we could not prove
any of them to be single axioms. For longer equations, we had
to be selective in generating equations because there are so many.
Table 2 lists five
jobs with the number of variables and the associations that were
considered. The notation f(m,n) means that we looked at
candidates f(t1,t2)=x, where length(t1)=m and length(t2)=n.

Table 2: MOL search
Job | Length | Variables | Associations |

23 | 23 | all | all |

25A | 25 | 3,4 | all |

25B | 25 | 5 | all |

27A | 27 | 4 | f(11,13) |

27B | 27 | 4 | f(9,15) |

The first MOL single axioms we found have length 27.
Several months later we proved that the following candidate
of length 25 is a single axiom.

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

## Completeness Proof (MOL)

Here is a (very long) proof, starting with `MOL-Sh`, and deriving
the MOL Sheffer 4-basis. This job uses hints to guide Otter directly to
a forward, demodulation-free proof.
otter < MOL-Sh.in > MOL-Sh.out

Here is a 2-part proof of the same theorem. The first part proves f(x,f(x,x)) = f(f(y,y),y)
which allows us to introduce a constant f(x,f(x,x)) = f(f(y,y),y) = 1, which simplifies the
second part. The number of steps is about the same, but the equations are much shorter.
otter < MOL-Sh-part1.in > MOL-Sh-part1.out
otter < MOL-Sh-part2.in > MOL-Sh-part2.out

## Soundness Proofs (MOL)

We give a soundness proof, that is, a proof that MOL-Sh
can be derived from the Sheffer MOL 4-basis.
otter < MOL-Sh-sound.in > MOL-Sh-sound.out