background image

Definition 52.

Infinitary pre-staroid

is such a staroid whose arity is infinite;

finitary pre-staroid

is such a staroid whose arity is finite.

Next we will define

completary staroids

. First goes the general case, next simpler case for the

special case of join-semilattices instead of arbitrary posets.

Definition 53.

A

completary staroid

is a poset relation conforming to the formulas:

1.

K

Q

form

f

: (

K

L

0

K

L

1

K

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

= 0

(

form

f

)

i

for some

i

arity

f

then

L

f

.

Lemma 54.

Every completary staroid is an upper set.

Proof.

Let

f

is a completary staroid. Let

L

0

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

f

and thus

L

1

f

because

L

1

L

0

L

1

L

1

.

Proposition 55.

A relation between posets whose form is a family of join-semilattices is a com-

pletary staroid iff both:

1.

L

0

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

= 0

(

form

f

)

i

for some

i

arity

f

then

L

f

.

Proof.

Let the formulas (1) and (2) hold. Then

f

is an upper set: Let

L

0

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

f

and

thus

L

1

=

L

0

L

1

f

.

Thus to finish the proof it is enough to show that

L

0

L

1

GR

f

⇔ ∀

K

Y

form

f

: (

K

L

0

K

L

1

K

GR

f

)

under condition that GR

f

is an upper set. But this is obvious.

Proposition 56.

A completary staroid is a staroid.

Proof.

Let

f

is a completary staroid.

Let

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

. Then

X

0

X

1

(

val

f

)

i

K

L

0

L

1

GR

f

⇔ ∃

k

∈ {

0

,

1

}

:

K

∪ {

(

i

;

X

k

)

} ∈

GR

f

K

∪ {

(

i

;

X

0

)

} ∈

f

K

∪ {

(

i

;

X

1

)

} ∈

GR

f

X

0

(

val

f

)

i

K

X

1

(

val

f

)

i

K

.

So

(

val

f

)

i

K

is a free star (taken in account that

K

i

= 0

(

form

f

)

i

f

K

).

f

is an upper set by the lemma.

Lemma 57.

Every finitary pre-staroid is completary.

Proof.

c

∈ {

0

,

1

}

n

: (

λi

n

:

L

c

(

i

)

i

)

GR

f

⇔ ∃

c

∈ {

0

,

1

}

n

1

: (

{

(

n

1;

L

0

(

n

1))

} ∪

(

λi

n

1:

L

c

(

i

)

i

))

GR

f

(

{

(

n

1;

L

1

(

n

1))

} ∪

(

λ i

n

1:

L

c

(

i

)

i

))

GR

f

⇔ ∃

c

∈ {

0

,

1

}

n

1

:

L

0

(

n

1)

(

val

f

)

n

1

(

λi

n

1:

L

c

(

i

)

i

)

L

1

(

n

1)

(

val

f

)

n

1

(

λi

n

1:

L

c

(

i

)

i

)

⇔ ∃

c

∈ {

0

,

1

}

n

1

K

Q

form

f

: (

K

L

0

(

n

1)

K

L

1

(

n

1)

K

(

val

f

)

n

1

(

λi

n

1:

L

c

(

i

)

i

))

⇔ ∃

c

∈ {

0

,

1

}

n

1

K

n

1

(

form

f

)

n

1

: (

K

n

1

L

0

(

n

1)

K

n

1

L

1

(

n

1)

⇒ {

(

n

1;

K

)

} ∪

(

λi

n

1:

L

c

(

i

)

i

))

GR

f

 

⇔ ∀

K

Q

form

f

: (

K

L

0

K

L

1

K

GR

f

)

.

Exercise 1.

Prove the simpler special case of the above theorem when the form is a family of join-semilattices.

Theorem 58.

For finite arity the following are the same:

1. pre-staroids;

2. staroids;

Definition of staroids

7