 3.7. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

49

Currying and uncurrying with a dependent variable.

Let

X

,

Z

be sets and

Y

be a function with the domain

X

. (Vaguely saying,

Y

is a variable dependent on

X

.)

The disjoint union

`

Y

=

S

i

dom

Y

(

{

i

} ×

Y

i

) =

n

(

i,x

)

i

dom

Y,x

Y

i

o

.

We will consider variables

x

X

and

y

Y

x

.

Let a function

f

Z

`

i

X

Y

i

(or equivalently

f

Z

`

Y

). Then curry(

f

)

Q

i

X

Z

Y

i

is the function defined by the formula (curry(

f

)

x

)

y

=

f

(

x, y

).

Let now

f

Q

i

X

Z

Y

i

. Then uncurry(

f

)

Z

`

i

X

Y

i

is the function defined

by the formula uncurry(

f

)(

x, y

) = (

f x

)

y

.

Obvious

288

.

1

. uncurry(curry(

f

)) =

f

for every

f

Z

`

i

X

Y

i

.

2

. curry(uncurry(

f

)) =

f

for every

f

Q

i

X

Z

Y

i

.

3.7.2.2.

Functions with ordinal numbers of arguments.

Let Ord be the set of

small ordinal numbers.

If

X

and

Y

are sets and

n

is an ordinal number, the set of functions taking

n

arguments on the set

X

and returning a value in

Y

is

Y

X

n

.

The set of all small functions taking ordinal numbers of arguments is

Y

S

n

Ord

X

n

.

I will denote OrdVar(

X

) =

f

S

n

Ord

X

n

and call it

. (“Var” in

this notation is taken from the word

in the collocation

used in computer science.)

3.7.3. On sums of ordinals.

Let

a

be an ordinal-indexed family of ordinals.

Proposition

289

.

`

a

with lexicographic order is a well-ordered set.

Proof.

Let

S

be non-empty subset of

`

a

.

Take

i

0

= min Pr

0

S

and

x

0

= min

n

Pr

1

y

y

S,y

(0)=

i

0

o

(these exist by properties of

ordinals). Then (

i

0

, x

0

) is the least element of

S

.

Definition

290

.

P

a

is the unique ordinal order-isomorphic to

`

a

.

Exercise

291

.

Prove that for finite ordinals it is just a sum of natural numbers.

This ordinal exists and is unique because our set is well-ordered.

Remark

292

.

An infinite sum of ordinals is not customary defined.

The

structured sum

L

a

of

a

is an order isomorphism from lexicographically

ordered set

`

a

into

P

a

.

There exists (for a given

a

) exactly one structured sum, by properties of well-

ordered sets.

Obvious

293

.

P

a

= im

L

a

.

Theorem

294

.

(

L

a

)(

n, x

) =

P

i

n

a

i

+

x

.

Proof.

We need to prove that it is an order isomorphism. Let’s prove it is an

injection that is

m > n

P

i

m

a

i

+

x >

P

i

n

a

i

+

x

and

y > x

P

i

n

a

i

+

y >

P

i

n

a

i

+

x

.

Really, if

m > n

then

P

i

m

a

i

+

x

P

i

n

+1

a

i

+

x >

P

i

n

a

i

+

x

. The second

formula is true by properties of ordinals.

Let’s prove that it is a surjection. Let

r

P

a

. There exist

n

dom

a

and

x

a

n

such that

r

= (

L

a

)(

n, x

). Thus

r

= (

L

a

)(

n,

0) +

x

=

P

i

n

a

i

+

x

because

(

L

a

)(

n,

0) =

P

i

n

a

i

since (

n,

0) has

P

i

n

a

i

predecessors.