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.
Therefore, there is no Sheffer stroke single axiom for
MOL of length less than 21.
- 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.
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,
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
These reduce the number of candidates to
Finally, by using the 9 OMLs that are not MOLs, up through size 16
(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
Although in general step 8 is unsound, in this case all of the candidates turn
out to be MOL identities
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
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