 Obvious 3.74.

1. uncurry

(

curry

(

f

)) =

f

for every

f

2

Z

X

Y

.

2. curry

(

uncurry

(

f

)) =

f

for every

f

2

(

Z

Y

)

X

.

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

ff

i

Y

i

j

i

2

dom

Y

g

=

f

(

i

;

x

)

j

i

2

dom

Y ; x

2

Y

i

g

.

We will consider variables

x

2

X

and

y

2

Y

x

.

Let a function

f

2

Z

`

i

2

X

Y

i

(or equivalently

f

2

Z

`

Y

). Then curry

(

f

)

2

Q

i

2

X

Z

Y

i

is the

function dened by the formula

(

curry

(

f

)

x

)

y

=

f

(

x

;

y

)

.

Let now

f

2

Q

i

2

X

Z

Y

i

. Then uncurry

(

f

)

2

Z

`

i

2

X

Y

i

is the function dened by the formula

uncurry

(

f

)(

x

;

y

) = (

fx

)

y

.

Obvious 3.75.

1. uncurry

(

curry

(

f

)) =

f

for every

f

2

Z

`

i

2

X

Y

i

.

2. curry

(

uncurry

(

f

)) =

f

for every

f

2

Q

i

2

X

Z

Y

i

.

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

2

Ord

X

n

.

I will denote OrdVar

(

X

) =

f

S

n

2

Ord

X

n

and call it

. (Var in this notation is

taken from the word

in the collocation

used in computer science.)

3.8.3 On sums of ordinals

Let

a

be an ordinal-indexed family of ordinals.

Proposition 3.76.

`

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

f

Pr

1

y

j

y

2

S ; y

(0) =

i

0

g

(these exist by properties of ordinals).

Then

(

i

0

;

x

0

)

is the least element of

S

.

Denition 3.77.

P

a

is the unique ordinal order-isomorphic to

`

a

.

[TODO: For nite ordinals

it is just a sum of natural numbers.]

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

Remark 3.78.

An innite sum of ordinals is not customary dened.

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

P

a

=

im

L

a

.

Theorem 3.80.

(

L

a

)(

n

;

x

) =

P

i

2

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

2

m

a

i

+

x >

P

i

2

n

a

i

+

x

and

y > x

)

P

i

2

n

a

i

+

y >

P

i

2

n

a

i

+

x

.

Really, if

m > n

then

P

i

2

m

a

i

+

x

>

P

i

2

n

+1

a

i

+

x >

P

i

2

n

a

i

+

x

. The second formula is true

by properties of ordinals.

Let's prove that it is a surjection. Let

r

2

P

a

. There exist

n

2

dom

a

and

x

2

a

n

such that

r

= (

L

a

)(

n

;

x

)

. Thus

r

= (

L

a

)(

n

; 0) +

x

=

P

i

2

n

a

i

+

x

because

(

L

a

)(

n

; 0) =

P

i

2

n

a

i

since

(

n

; 0)

has

P

i

2

n

a

i

predecessors.

44

More on order theory