eyeprolog

Greatest lower bounds are unique

If two things are both the greatest lower bound of the same pair, are they the same?

A classic lemma of order theory, written as rules. Two names, g1 and g2, are both declared the greatest lower bound of a and b; the rules derive that each lies below the other, and therefore that they denote the same element.

Run it in the playground · Source

The question

In an ordered set, a lower bound of a and b is anything below both. The greatest lower bound (GLB) is the lower bound that every other lower bound lies below. Mathematicians prove it is unique: two GLBs must each be below the other, and in a partial order that makes them equal (antisymmetry).

The example runs that argument on concrete names.

The facts and rules

glbOf(g1, a, b).
glbOf(g2, a, b).

lowerBoundOf(M, A, B) :- glbOf(M, A, B).

leq(L, M) :-
  glbOf(M, A, B),
  lowerBoundOf(L, A, B).

sameTerm(M, N) :-
  leq(M, N),
  leq(N, M).

leq/2 is the defining property of a GLB: any lower bound L is below the GLB M. sameTerm/2 is antisymmetry: below each other means the same.

The conclusion

sameGreatestLowerBound(A, B, M, N) :-
  glbOf(M, A, B),
  glbOf(N, A, B),
  sameTerm(M, N),
  (M \= N).

The M \= N test keeps only the interesting answers, where two different names turn out to denote the same bound.

The answer

eyeprolog examples/greatest-lower-bound-uniqueness.pl

sameGreatestLowerBound(a, b, g1, g2).
sameGreatestLowerBound(a, b, g2, g1).

The relation is symmetric, so the conclusion appears once in each direction.

The reason

step(sameTerm(g1, g2), rule(5), ['M' = g1, 'N' = g2], [leq(g1, g2), leq(g2, g1)]).
step(leq(g1, g2),
     rule(4),
     ['L' = g1, 'M' = g2, 'A' = a, 'B' = b],
     [glbOf(g2, a, b), lowerBoundOf(g1, a, b)]).

g1 and g2 are the same because each is below the other. g1 is below g2 because g2 is a GLB of a and b, and g1 is a lower bound of them. This is the textbook proof, one step per line.

The check

condition('C1', resolution, ok, 10).
condition('C5', re_decision, ok, 2).
verdict(checked).

The 10 rule and fact steps replay against their clauses, and the two g1 \= g2 tests were recomputed and agreed. Nothing is trusted.

Try it

Add a third name, glbOf(g3, a, b). How many answers now? (Six: every ordered pair of distinct names.)
Remove lowerBoundOf/3 and say which step of the mathematical argument goes missing.

Learn more in The Art of EyeProlog, Chapter 28.

This site is open source. Improve this page.