 Toward formalization of partial infima and suprema

by Victor Porton

Let

(

A

;

6

)

be a partially ordered set. Let

A

,

B

be subsets of

A

.

Consider the following statement:

Statement 1.

sup

A

=

sup

B

whenever sup

A

is defined.

Statements like this are often encountered in informal mathematics. But it is problematic to
describe it formally, as many important formal systems (and proof assistent languages) do not
include the notion of partially defined function.

The most trivial way to formalize it without resorting to partial functions is:

Statement 2.

Whenever some

x

A

is a supremum of

A

,

x

is also a supremum of

B

.

This allows to formalize the initial statement, but this way has a deficiency that clear and concise
equality is replaced with words and a quantifier

(expressed here as the word “whenever”).

A fascinating way to formalize this with algebraic formulas, without quantifiers is to use Dedekind-
MacNeille completion.

Let

B

is the Dedekind-MacNeille completion of

A

. Let

γ

is the order embedding of this completion

from

A

to

B

. Let

A

is the image of

A

in

B

. Note that

γ

is an isomorphism from

A

to

A

.

It is well known that

γ

preserves all existing infima and suprema in

A

. (I confess that I never read

a proof of this statement.)

Thus our statement can be rewritten:

Statement 3.

sup

γ

[

A

]

A

sup

γ

[

A

] =

sup

γ

[

B

]

.

So our statement is rewritten as a simple propositional formula (without quantifiers), reasoning
about some sets in

B

. We can get back our statement (say “statement 2”) knowing properties of

suprema and infima in complete lattice

B

.

For the people doing formalization of order theory I suggest to write both:

statement 3 (with

γ

[

A

]

and

γ

[

B

]

replaced with some more direct expressions of some subsets

of

B

);

statement 2 (possibly as a corollary of statement 3 which may be probably simpler to prove).

Well, the work not yet possibly done is to formalize Dedekind-MacNeille completion and prove
that it preserves all existing infima and suprema.

1