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