background image

Proof.

We need to prove that

λi

dom

A

:

a

i

#

b

i

=

d

{

z

Q

A

|

z

a

z

b

}

.

To prove it is enough to show

a

i

#

b

i

=

d

{

z

i

|

z

Q

A

, z

a

z

b

}

that is

a

i

#

b

i

=

d

{

z

A

i

|

z

a

i

∧ ∀

j

dom

A

:

z

j

b

j

}

that is

a

i

#

b

i

=

d

{

z

A

i

|

z

a

i

z

b

i

}

(take

z

i

= 0

for

j

i

) what is true by definition.

Proposition 40.

Let every

A

i

is a poset with least element and

a

i

is defined. Then

a

=

λi

n

:

a

i

.

Proof.

We need to prove that

λi

dom

A

:

a

i

=

F

{

c

A

|

c

a

}

. To prove this it is enough to show

that

a

i

=

F

{

c

i

|

c

A

, c

a

}

that is

a

i

=

F

{

c

i

|

c

A

,

j

n

:

c

j

a

j

}

that is

a

i

=

F

{

c

i

|

c

A

,

c

i

a

i

}

(take

c

i

= 0

for

j

i

) that is

a

i

=

F

{

c

A

|

c

a

i

}

what is true by definition.

Corollary 41.

Let every

A

i

is a poset with least element and

a

i

+

is defined. Then

a

+

=

λi

n

:

a

i

+

.

Proof.

By duality.

5 Definition of staroids

Let

n

be a set. As an example,

n

may be an ordinal,

n

may be a natural number, considered as a

set by the formula

n

=

{

0

,

 

, n

1

}

. Let

A

=

A

i

n

is a family of posets indexed by the set

n

.

Definition 42.

I will call an

anchored relation

a pair

f

= (

form

f

;

GR

f

)

of a family form

(

f

)

of

sets indexed by the some index set and a relation GR

(

f

)

P

Q

form

(

f

)

. I call GR

(

f

)

the

graph

of the anchored relation

f

. I denote Anch

(

A

)

the set of small anchored relations of the form

A

.

Definition 43.

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 44.

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

f

g

GR

f

GR

g

.

Definition 45.

An anchored relation is an

anchored relation between posets

when every

(

form

f

)

i

is a poset.

Definition 46.

Let

f

is an anchored relation. For every

i

arity

f

and

L

Q

((

form

f

)

|

(

arity

f

)

\{

i

}

)

(

val

f

)

i

L

=

{

X

(

form

f

)

i

|

L

∪ {

(

i

;

X

)

} ∈

GR

f

}

(“val” is an abbreviation of the word “value”.)

Obvious 47.

X

(

val

f

)

i

L

L

∪ {

(

i

;

X

)

} ∈

GR

f

.

Proposition 48.

f

can be restored knowing form

(

f

)

and

(

val

f

)

i

for some

i

n

.

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 49.

A

pre-staroid

is an anchored relation

f

between poset such that

(

val

f

)

i

L

is a free

star for every

i

arity

f

,

L

Q

(

form

f

)

|

(

arity

f

)

\{

i

}

.

Definition 50.

A

staroid

is a pre-staroid whose graph is an upper set (on the poset if anchored

relations of the form of this pre-staroid).

Proposition 51.

If

L

Q

form

f

and

L

i

= 0

(

form

f

)

i

for some

i

arity

f

then

L

f

if

f

is an pre-

staroid.

Proof.

Let

K

=

L

|

(

arity

f

)

\{

i

}

. We have

0

(

val

f

)

i

K

;

K

∪ {

(

i

; 0)

}

f

;

L

f

.

6

Section 5