# 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.
 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
```