 21.2. DEFINITION OF STAROIDS

321

Proposition

1643

.

An anchored relation

f

between posets whose form is a

family of join-semilattices is a completary staroid iff both:

1

.

L

0

t

L

1

GR

f

⇔ ∃

c

∈ {

0

,

1

}

n

: (

λi

n

:

L

c

(

i

)

i

)

GR

f

for every

L

0

, L

1

Q

form

f

.

2

. If

L

Q

form

f

and

L

i

=

(form

f

)

i

for some

i

arity

f

then

L /

GR

f

.

Proof.

Let the formulas

1

and

2

hold. Then

f

is an upper set: Let

L

0

v

L

1

for some

L

0

, L

1

Q

form

f

and

L

0

f

. Then taking

c

=

n

× {

0

}

we get

λi

n

:

L

c

(

i

)

i

=

λi

n

:

L

0

i

=

L

0

GR

f

and thus

L

1

=

L

0

t

L

1

GR

f

.

Thus to finish the proof it is enough to show that

L

0

t

L

1

GR

f

⇔ ∀

K

Y

form

f

: (

K

w

L

0

K

w

L

1

K

GR

f

)

under condition that GR

f

is an upper set. But this equivalence is obvious in both

directions.

Proposition

1644

.

Every completary staroid is a staroid.

Proof.

Let

f

be a completary staroid.

Let

i

arity

f

,

K

Q

i

(arity

f

)

\{

i

}

(form

f

)

i

. Let

L

0

=

K

∪ {

(

i, X

0

)

}

,

L

1

=

K

∪ {

(

i, X

1

)

}

for some

X

0

, X

1

A

i

.

Let

Z

A

i

: (

Z

w

X

0

Z

w

X

1

Z

(val

f

)

i

K

);

then

Z

A

i

: (

Z

w

X

0

Z

w

X

1

K

∪ {

(

i, Z

)

} ∈

GR

f

)

.

If

z

w

L

0

z

w

L

1

then

z

w

K

∪ {

(

i, z

i

)

}

, thus taking into account that GR

f

is an

upper set,

z

Y

A

: (

z

w

L

0

z

w

L

1

K

∪ {

(

i, z

i

)

} ∈

GR

f

)

.

z

Y

A

: (

z

w

L

0

z

w

L

1

z

GR

f

)

.

Thus, by the definition of completary staroid,

L

0

GR

f

L

1

GR

f

that is

X

0

(val

f

)

i

K

X

1

(val

f

)

i

K.

So (val

f

)

i

K

is a free star (taken into account that

z

i

=

(form

f

)

i

z /

GR

f

and

that (val

f

)

i

K

is an upper set).

Exercise

1645

.

Write a simplified proof for the case if every (form

f

)

i

is a

join-semilattice.

Lemma

1646

.

Every finitary prestaroid is completary.