 21.4. PRINCIPAL STAROIDS

323

Proposition

1651

.

(val

f

)

i

L

= (val

f

)

i

L

Z

i

for every

L

Q

Z

|

(arity

f

)

\{

i

}

.

Proof.

(val

f

)

i

L

=

X

Z

i

L

∪{

(

i,X

)

}∈

GR

f

Q

Z

=

n

X

Z

i

L

∪{

(

i,X

)

}∈

GR

f

o

=

(val

f

)

i

L

Z

i

.

Proposition

1652

.

Let (

A

i

,

Z

i

) be binarily join-closed filtrators with both the

base and the core being join-semilattices. If

f

is a staroid of the form

A

, then

f

is a staroid of the form

Z

.

Proof.

Let

f

be a staroid.

We need to prove that (val

f

)

i

L

is a free star. It follows from the last

proposition and the fact that it is binarily join-closed.

Proposition

1653

.

Let each (

A

i

,

Z

i

) for

i

n

(where

n

is an index set) be a

binarily join-closed filtrator, such that each

A

i

and each

Z

i

are join-semilattices. If

f

is a completary staroid of the form

A

then

f

is a completary staroid of the

form

Z

.

Proof.

L

0

t

Z

L

1

GR

f

L

0

t

Z

L

1

GR

f

L

0

t

A

L

1

GR

f

c

∈ {

0

,

1

}

n

: (

λi

n

:

L

c

(

i

)

i

)

GR

f

c

∈ {

0

,

1

}

n

: (

λi

n

:

L

c

(

i

)

i

)

GR

f

for every

L

0

, L

1

Q

Z

.

21.4. Principal staroids

Definition

1654

.

The

staroid generated

by an anchored relation

F

is the

staroid

f

=

Strd

F

on powersets such that

↑ ◦

L

GR

f

Q

L

6

F

and (form

f

)

i

=

T

(form

F

)

i

for every

L

Q

i

arity

f

T

(form

F

)

i

.

Remark

1655

.

Below we will prove that staroid generated by an anchored

relation is a staroid and moreover a completary staroid.

Definition

1656

.

A

principal staroid

is a staroid generated by some anchored

relation.

Proposition

1657

.

Every principal staroid is a completary staroid.

Proof.

That

L /

GR

f

if

L

i

=

(form

f

)

i

for some

i

arity

f

is obvious. It

remains to prove

Y

(

L

0

t

L

1

)

6

F

⇔ ∃

c

∈ {

0

,

1

}

arity

f

:

Y

i

n

L

c

(

i

)

i

6

F.