20. ALTERNATIVE REPRESENTATIONS OF BINARY RELATIONS

313

Figure 1.

binary relations

between

A

and

B

pointfree funcoids

between

P

A

and

P

B

antitone Galois

connections

between

P

A

and

P

B

Galois connections

between

P

A

and

P

B

Ψ

1

1

Ψ

2

Ψ

1

2

Ψ

3

Ψ

4

Ψ

1

Ψ

1

3

Ψ

5

1

5

Ψ

1

4

Ψ

1

.

f

7→

n

(

x,y

)

y

f

0

{

x

}

o

=

n

(

x,y

)

x

f

1

{

y

}

o

Ψ

1

1

.

r

7→

X

7→

n

y

B

x

X

:

xry

o

, Y

7→

n

x

A

y

Y

:

xry

o

Ψ

2

.

r

7→

(

P

A,

P

B,

h

r

i

,

r

1

)

Ψ

1

2

.

f

7→

n

(

x,y

)

{

x

}

[

f

]

{

y

}

o

Ψ

3

.

f

7→

X

7→

d

x

T

X

\{⊥}

h

f

i

x, Y

7→

d

y

T

Y

\{⊥}

f

1

y

=

X

7→

d

x

X

h

f

i{

x

}

, Y

7→

d

y

Y

f

1

{

y

}

Ψ

1

3

.

f

7→

P

A,

P

B, X

7→

d

x

T

X

\{⊥}

f

0

x, Y

7→

d

y

T

Y

\{⊥}

f

1

y

=

P

A,

P

B, X

7→

d

x

X

f

0

{

x

}

, Y

7→

d

y

Y

f

1

{

y

}

Ψ

4

.

f

7→

X

7→ ¬

d

x

T

X

\{⊥}

h

f

i

x, Y

7→

d

y

T

Y

\{⊥}

f

1

¬

y

=

X

7→

d

x

T

X

\{⊥}

¬h

f

i

x, Y

7→

d

y

T

Y

\{⊥}

f

1

¬

y

=

X

7→ ¬

d

x

X

h

f

i{

x

}

, Y

7→

d

y

Y

f

1

¬{

y

}

=

X

7→

d

x

X

¬h

f

i{

x

}

, Y

7→

d

y

Y

f

1

¬{

y

}

Ψ

1

4

.

f

7→

P

A,

P

B, X

7→

d

x

T

X

\{⊥}

¬

f

0

x, Y

7→

d

y

T

Y

\{⊥}

f

1

¬

y

=

P

A,

P

B, X

7→ ¬

d

x

T

X

\{⊥}

f

0

x, Y

7→

d

y

T

Y

\{⊥}

f

1

¬

y

=

P

A,

P

B, X

7→

d

x

X

¬

f

0

{

x

}

, Y

7→

d

y

Y

f

1

¬{

y

}

=

P

A,

P

B, X

7→ ¬

d

x

X

f

0

{

x

}

, Y

7→

d

y

Y

f

1

¬{

y

}

Ψ

5

= Ψ

1

5

.

f

7→

(

¬ ◦

f

0

, f

1

◦ ¬

)

Claim: Ψ

1

maps antitone Galois connections between

P

A

and

P

B

into binary

relations between

A

and

B

.

Proof: Obvious.

Claim: Ψ

1

1

maps binary relations between

A

and

B

into antitone Galois connec-

tions between

P

A

and

P

B

.

Proof: We need to prove

Y

n

y

B

x

X

:

xry

o

X

n

x

A

y

Y

:

xry

o

. After we equiva-

lently rewrite it:

y

Y

x

X

:

x r y

⇔ ∀

x

X

y

Y

:

x r y