Prover9 Examples: Distributivity in Median Algebras

For more detail on this, see Bob Veroff's median algebra page.

Median Algebras

A median algebra has a ternary operation satisfying the following axioms.

   f(x,x,y) = x                       # label(majority).
   f(x,y,z) = f(z,x,y)                # label(2a).
   f(x,y,z) = f(x,z,y)                # label(2b).
   f(f(x,w,y),w,z) = f(x,w,f(y,w,z))  # label(associativity).

Notes about the axioms.

(2a) and (2b) allow the arguments of f to be permuted in any way (trivial).
(2b) is dependent on the remaining three axioms, so it can be removed.
Proof:
prover9 -f dep-2b.in > dep-2b.out ; ### ( dep-2b.out.xml )
The remaining three are independent.
If we permute the arguments in the associativity axiom in the right ways, we can do without the permutativity axioms. For example, an equivalent 2-basis is
```
     f(x,x,y) = x                        # label(majority).
     f(f(x,w,y),z,w) = f(w,x,f(w,z,y))   # label(associativity2).
```
We can prove this by deriving (2a) and (2b):
prover9 -f 2basis.in > 2basis.out ; ### ( 2basis.out.xml )

Ternary Distributivity Properties

The following two distributrivity properties hold for median algebras.

   f(f(x,y,z),u,w) = f(x,       f(y,u,w),f(z,u,w))    # label(dist_short).
   f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w))    # label(dist_long).

A higher-order proof was given by M. Kolibiar and T. Marcisova in 1974.

The first equational proof we know of was found by Bob Veroff and Otter.

A proof by Prover9:

prover9 -f dist-both.in > dist-both.out ; ### ( dist-both.out.xml )

Given one of the distributivity properties, prove the other.

Short implies long.

prover9 -f dist-short-long.in > dist-short-long.out ; ### ( dist-short-long.out.xml )

Long implies short.

prover9 -f dist-long-short.in > dist-long-short.out ; ### ( dist-long-short.out.xml )