Finding Countermodels

Back to the Main Page

Given a candidate that passed all of the current filters, we asked Mace to find countermodels to serve as filters for the given candidate and subsequent candidates.

1 Basic Countermodels

Some of the initial countermodels were found be asking Mace4 for models of candidates failing basic (Sheffer stroke) properties of ortholattices such as commutativity, absoprtion, existence of a ONE, or simply by asking for a model of odd size.

Other countermodels were found with Mace4 by giving a candidate, stating that some of the properties of OLs hold, and other OL properties fail. For example,

    mace4 -N10 < OL-cand-c1.in > OL-cand-c1.out

These methods produced many models, up through size 8. Many of filters became redundant, however, because later models would do the jobs of earlier models. Because we were filtering large numbers of candidates, we wished to keep the number of filters small, so we eliminated many of the redundant filters. We arrived at the filter sets non-OL.A-4 and non-OL.B-9 in this way.

2 Highly Constrained Countermodels

2.1 Quasigroup Models

A quasigroup is set with a binary operation that is left and right solvable. That is,
    all x all y exists z (x * z = y).
    all x all y exists z (z * x = y).
The Sheffer stroke operation of a nontrivial ortholattice cannot be a quasigroup. Therefore any OL, OML, or MOL candidate with a nontrivial quasigoup model cannot be a single axiom.

Here is an example. Consider the OML candidate

    f(f(f(y,x),x),f(f(f(z,x),f(y,x)),f(f(y,y),z))) = x.
This candidate passed the filters non-OL.A-4 and non-OL.B-9. Mace4 searches for noncommutative models failed (allowing several hours), but a Mace4 search for a quasigroup model quickly found a quasigroup of size 7, which happens to be noncommutative:
    mace4 -N10 < OML-cand-qg.in > OML-cand-qg.out
That structure became a member of non-OL.C-23.

2.2 Nonmodular OMLs

When filtering MOL candidates, the nonmodular OMLs turned out to be useful. In the table of OLs, these are simply the OMLs that are not MOLs. A quick way to obtain them is to remove the modular lattices from the sets of OMLs by using the program interpfilter as follows. The following example gets the nonmodular OMLs of size 16.
    interpfilter modularity nonmodels < OML.16 > nonmod-OML.16

3 Summary of Steps 8 and 9

The table below shows the structures that were used in Steps 8 and 9 of the generate-and-filter procedure. Recall that Step 8 eliminates (some or all of the) equations that are too strong to be identities, and Step 9 eliminates some of the equations that are too weak to be single axioms.

Filters for Steps 8 and 9
Theory Size Step-8 Step-9
OL all OL decision procedure non-OL.A-4
OML <= 19 OML.6 non-OL.B-9
21,23 OML.6
OML.10
non-OL.C-23
MOL <= 19 MOL.6 (= OML.6) non-OL.B-9
21,23,25,27 MOL.6 (= OML.6) non-OL.C-23
non-OL.D-14
non-MOL-OML
Notes on the table.