On Lambda Calculus and Ordinal Numbers (Part 2)

So we're going to take a little detour and forget about functions for a moment. Instead, we're going to talk about ordinals. First, we need to talk about ordered sets really quick.

An ordered set is a set with order. I know...

So, a set is any collection of objects within the universe of discourse (i.e. if we're talking about numbers, we can't have a set with plates; but if we're talking about dishes we can't have a set with numbers). Typically, order doesn't matter, so the set {1,2,3} is the same as the set {2,3,1}. Also, the number of times an element shows up doesn't matter, so {1,1,1,2,3} is the same as {1,2,3} (is the same as {2,3,1}).

In an ordered set, the order does matter. Some relation applies to each set of two differentelements. I don't use the word pair, because in a mathematical pair, (a,b) is not the same as (b,a). Either a < b or b< a.
To be more for formal. Define a relation < on a set S. For any distinct members a,b of S, either (a,b) is in < , or (b,a) is in < .

An ordered set is well-ordered if the set, and every subset (ordered by the same relation) of it has a first element. For example the integers (including negative integers) ordered according to the normal definition of "< " are not well-ordered, because it does not have a first element. Neither are the natural numbers ordered backwards (i.e. {...,3,2,1,0}).
But the natural numbers ordered normally are, since any subset will have a first element.

An ordinal number is a "number" which designates a well-ordered set. (Well, any well-ordered set that satisfies the same properties).

Anyway, avoiding all the definitions and proofs, when you add two ordinals, attach the second set to the end of the first set. and "rename" the elements to avoid repetition. Notice that this is not commutative-- a+b is not necessarily the same as b+a.

Also, before you ask, numbers are defined as the set of all numbers that are before it in the usual ordering of the naturals. 0={} (empty set), 1={0} = {{}}, 2={0,1}, etc.

For example 1+ω (ω meaning infinity) is {0,0,1,2,...}. Renaming all of the elements after the first one gives us {0,1,2,...} = ω
However, +1 gives is {0,1,2,3,...,1}. The last element can't be relabeled to the "next element of ω" because ω has no last element. So we make 1 into 1' (or something) so we have {0,1,...,1'}, which is still infinite but has a first and a last element, so is not ω.

[note: from now on the relabeling of identical elements will be assumed, so ω+1={0,1,2,...,1} will be acceptable)

Now, multiplication works similarly. In a*b, a is appended to itself b times. E.g.
2*4 = {0,1,0,1,0,1,0,1} (with proper relabeling).

Again, 2*ω = {0,1,0,1,.....} Again, we get 2*ω = ω
But, ω*2 = {0,1,2,...,0,1,2,}. This is ω+ω which is not the same as ω, because we have two disjoint maximal subsets with no last element.

That's really all we need to know about ordinals: addition and multiplication are non-commutative, and for any finite a, a*ω = a+ω = ω, and ω*a = ω+ω+...+ω, (a times).

Now that that is out of the way, we can look back at lambda calculus.

The first thing to notice is that everything has a successor and a predecessor (There's a function for that, but it's messy and we don't need to see it.) And if a comes before b, and b comes before c, then a comes before c. Also, the predecessor of 0 is o-- which is to say, 0 is the first element.

What I'm trying to say is that each of the natural numbers in LC represents an ordinal number.
I said earlier that Y might act like an ordinal number. Namely, ω:
ω=Y=λf.(λx.f(xx)) λx.f(xx)
Since I haven't actually described how this works.Yf takes a function and returns f(Yf). That is, it returns itself with an extra f out front; where f is the function it was given. This also means that ff(Yf) -> f...ff(Yf). Hurray! An infinite number of f's.

We need to see if this is actually a valid encoding of ω. So, we need to make sure all of the following hold:
1+ω=ω, 2*ω=ω, ω+1 is distinct from ω, and ω*2=ω+ω.

Let's look back at our definition.
Addition:
plus m n := λm.λn.λf.λa. m f (n f a)
Multiplication:
times m n := λm.λn.λf. m (n f)

1+Y:
-> λf.λa. 1 f (Y f a) -> λf.λa. f (Y f a). There are a few rules of LC that allow us to throw out the a. I'm not sure how to describe them easily. It has to do with free and bound variables... I'll let you figure that out.
Anyway,
-> λf.f(Yf) which is what Yf "reduces" to. So 1+Y holds as expected

Y+1:
λf.λa. Y f (1 f a) -> λf. λa. Y f fa -> λf.λa.f (Yf) fa
The fa at the end don't go in the (Yf) parenthesis, because Y doesn't use them.
So what we have is equivalent to
λf. (Yf) f.
The a can be thrown out, but not the f, since it's the same as the argument to Y. This means, we have an extra f at the end. I.e. Y is not Y+1.

2*Y:
λf. Y (2 f) -> λf. (Y (ff))
This is our own major problem. I'm not entirely sure what to do with this, and it isn't going to reduce to (Yf) unless I'm very much mistaken.

Y*2:
λf. 2 (Yf). -> λf.(Yf)(Yf)

Y+Y = λf.λa. Y f (Y f a). Again, this becomes:
λf. Yf (Yf), rearranging our notation:
λf. (Yf)(Yf)

So we have a tricky 2*Y. Does that mean Y isn't ω? Probably. Does that mean Y isn't infinite? No. Especially since 2*Y is still going to end up infinite.
I doesn't matter anyway, since Delaney was talking about addition, and this clearly holds for Y=ω.

Future things:
Figure out how to do 2*Y. Figure out how to encode sets and cardinals in LC.