 21.2. DEFINITION OF STAROIDS

320

Definition

1631

.

Infinitary anchored relation

is such an anchored relation

whose arity is infinite;

finitary anchored relation

is such an anchored relation whose

arity is finite.

Definition

1632

.

An anchored relation

on powersets

is an anchored relation

f

such that every (form

f

)

i

is a powerset.

I will denote arity

f

= dom form

f

.

Definition

1633

.

[

f

]

is the relation between typed elements

T

(form

f

)

i

(for

i

arity

f

) defined by the formula

L

[

f

]

T

L

GR

f

.

Every set of anchored relations of the same form constitutes a poset by the

formula

f

v

g

GR

f

GR

g

.

Definition

1634

.

An anchored relation is an

anchored relation between posets

when every (form

f

)

i

is a poset.

Definition

1635

.

(val

f

)

i

L

=

n

X

(form

f

)

i

L

∪{

(

i,X

)

}∈

GR

f

o

.

Proposition

1636

.

f

can be restored knowing form(

f

) and (val

f

)

i

for some

i

arity

f

.

Proof.

GR

f

=

K

Q

form

f

K

GR

f

=

L

∪ {

(

i, X

)

}

L

Q

(form

f

)

|

(arity

f

)

\{

i

}

, X

(form

f

)

i

, L

∪ {

(

i, X

)

} ∈

GR

f

=

L

∪ {

(

i, X

)

}

L

Q

(form

f

)

|

(arity

f

)

\{

i

}

, X

(val

f

)

i

L

.

Definition

1637

.

A

prestaroid

is an anchored relation

f

between posets such

that (val

f

)

i

L

is a free star for every

i

arity

f

,

L

Q

(form

f

)

|

(arity

f

)

\{

i

}

.

Definition

1638

.

A

staroid

is a prestaroid whose graph is an upper set (on

the poset

Q

form(

f

)).

Definition

1639

.

A

(pre)staroid on power sets

is such a (pre)staroid

f

that

every (form

f

)

i

is a lattice of all subsets of some set.

Proposition

1640

.

If

L

Q

form

f

and

L

i

=

(form

f

)

i

for some

i

arity

f

then

L /

GR

f

if

f

is a prestaroid.

Proof.

Let

K

=

L

|

(arity

f

)

\{

i

}

. We have

/

(val

f

)

i

K

;

K

∪ {

(

i,

)

}

/

GR

f

;

L /

GR

f

.

Next we will define

completary staroids

. First goes the general case, next sim-

pler case for the special case of join-semilattices instead of arbitrary posets.

Definition

1641

.

A

completary staroid

is an anchored relation between posets

conforming to the formulas:

1

.

K

Q

form

f

: (

K

w

L

0

K

w

L

1

K

GR

f

) is equivalent to

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

.

Lemma

1642

.

Every graph of completary staroid is an upper set.

Proof.

Let

f

be a completary staroid. Let

L

0

v

L

1

for some

L

0

, L

1

Q

form

f

and

L

0

GR

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

GR

f

because

L

1

w

L

0

L

1

w

L

1

.