Single Axiom for Ortholattices
Back to the Main Page
Summary. There there is no OL Sheffer stroke axiom of length
less than 23. We present an axiom of length 23 with 4 variables,
and we show that every Sheffer stroke axiom of length 23
has at least 4 variables.
OL Candidates, Up Through Length 21
We have a decision procedure for OL, and
Table 2 contains the OL identities satisfying properties 1--8.
The sets do not contain alphabetic variants, but they do contain
many that are subsumed by others in the same set.
Table 2: OL Identities
The four non-ortholattices
eliminate all of the OL candidates in Table 2,
showing that there is no Sheffer stroke single axiom for OL
of length < 23.
|Length||Number of Candidates|
| <= 11
OL search, Length 23
Applying the same method and filter to the 3 and 4 variable
equations of length 23 yields
All of those candidates have 4 variables.
Since that set is complete for 3 and 4 variables, all length 23
Sheffer stroke single axioms have at least 4 variables.
does that and then sends those candidates to ploop3 which
calls Otter for each candidate.
Otter proved that two of the 540 candidates are single axioms.
Here is the first.
f(f(f(f(y,x),f(x,z)),u),f(x,f(f(x,f(f(y,y),y)),z))) = x. % OL-Sh
Completeness Proofs (OL)
By completeness proof we mean a proof of a known basis from
Here are two completeness proofs. The first proves the
Sheffer stroke OL 3-basis from OL-sax,
and the second proves the join/complement 5-basis.
otter < OL-Sh.in > OL-Sh.out
otter < OL-Sh-jc.in > OL-Sh-jc.out
Soundness Proofs (OL)
By soundness proof we mean a proof that the candidate is valid in the
We give two soundness proofs.
The first proves OL-sax from the Sheffer OL 3-basis,
and the second proves it from the join/complement
otter < OL-Sh-sound.in > OL-Sh-sound.out