 CHAPTER 4

Typed sets and category Rel

4.1. Relational structures

Definition

355

.

A

relational structure

is a pair consisting of a set and a tuple

of relations on this set.

A poset (

A

,

v

) can be considered as a relational structure: (

A

,

J

v

K

)

.

A set can

X

be considered as a relational structure with zero relations: (

X,

JK

)

.

This book is not about relational structures. So I will not introduce more

examples.

Think about relational structures as a common place for sets or posets, as far

as they are considered in this book.

We will denote

x

(

A

, R

) iff

x

A

for a relational structure (

A

, R

).

4.2. Typed elements and typed sets

We sometimes want to differentiate between the same element of two different

sets. For example, we may want to consider different the natural number 3 and the

rational number 3. In order to describe this in a formal way we consider elements

of sets together with sets themselves. For example, we can consider the pairs (

N

,

3)

and (

Q

,

3).

Definition

356

.

A

typed element

is a pair (

A

, a

) where

A

is a relational struc-

ture and

a

A

.

I denote type(

A

, a

) =

A

and GR(

A

, a

) =

a

.

Definition

357

.

I will denote typed element (

A

, a

) as @

A

a

or just @

a

when

A

is clear from context.

Definition

358

.

A

typed set

is a typed element equal to (

P

U, A

) where

U

is

a set and

A

is its subset.

Remark

359

.

Typed sets

is an awkward formalization of type theory sets in

ZFC (

U

is meant to express the

type

of the set). This book could be better written

using type theory instead of ZFC, but I want my book to be understandable for

everyone knowing ZFC. (

P

U, A

) should be understood as a set

A

of type

U

. For

an example, consider (

P

R

,

[0; 10]); it is the closed interval [0; 10] whose elements

are considered as real numbers.

Definition

360

.

TA

=

n

(

A

,a

)

a

A

o

=

{

A

} ×

A

for every relational structure

A

.

Remark

361

.

TA

is the set of typed elements of

A

.

Definition

362

.

If

A

is a poset, we introduce order on its typed elements

isomorphic to the order of the original poset: (

A

, a

)

v

(

A

, b

)

a

v

b

.

Definition

363

.

I denote GR(

A

, a

) =

a

for a typed element (

A

, a

).

Definition

364

.

I will denote

typed subsets

of a typed poset (

P

U, A

) as

P

(

P

U, A

) =

n

(

P

U,X

)

X

P

A

o

=

{

P

U

} ×

P

A

.

61