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
| Length | Number of Candidates |
| <= 11 |
0 |
| 13 |
3 |
| 15 |
26 |
| 17 |
466 |
| 19 |
4685 |
| 21 |
70659 |
The four non-ortholattices
interps/non-OL.A-4
eliminate all of the OL candidates in Table 2,
showing that there is no Sheffer stroke single axiom for OL
of length < 23.
OL search, Length 23
Applying the same method and filter to the 3 and 4 variable
equations of length 23 yields
540 candidates.
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.
The script
enumerate/OL/23/go
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
the candidate.
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
theory.
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
OL 5-basis.
otter < OL-Sh-sound.in > OL-Sh-sound.out