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
OML	21,23	OML.6 OML.10	non-OL.C-23
MOL	<= 19	MOL.6 (= OML.6)	non-OL.B-9
MOL	21,23,25,27	MOL.6 (= OML.6)	non-OL.C-23 non-OL.D-14 non-MOL-OML

Notes on the table.

For Step 8, we list only the models that contributed to the filtering. In many cases, we input additional models that did not contribute. For example, we tried all of our OMLs and MOLs for size 21 candidates; the additional ones did not contribute any filtering, so we did not use them for the larger candidates.
The non-OL models A-4, B-9, and C-23 are not disjoint, and there is no subset relation among them. They turned out this way, because we sought minimal sets that would do the job for the various cases.
The set D-14 is disjoint from each of A-4, B-9, and C-23.