Mathworks (Not the main chat!) - 2017-10-21

« first day (29 days earlier) ← previous day next day → last day (470 days later) »

8:09 AM

in Mathematics, 4 mins ago, by Secret

37 mins ago, by Secret

0,1,2,....$\omega$,...,$\omega_{\omega}$,...,$\beth_{\beth_{\omega}}$,..........‌....,0

The above cyclically ordered set is constructed by taking the ordinals in their usual ordering, and adding the following extra relation:

$\forall \alpha \in \Bbb{On},\alpha < 0$

Therefore this set is not ordered by $\in$

The predicative version:

$0,1,2,....,\omega,.....0$

where the ordering for those ordinal like terms is only a partial ordering as outlined in this and following block of comments:

2 days ago, by user21820

However, if you mean the equivalence classes of well-orderings under isomorphism, then you have a problem even constructing that because you can't assume (without LEM) that any two well-orderings are either isomorphic or not. However, isomorphism is still a pseudo equivalence relation on well-orderings in the sense that you only lack total ordering. So you still can go ahead and construct the type WO = { { (T,◁) : (S,<) is isomorphic to (T,◁) } : (S,<) is a well-order }.

@Secret Um I don't know what you mean by "following block of comments", since all the comments after the one you quoted are concerning ORD, which is incompatible with WO.

Specifically, WO is defined without any form of replacement. ORD can too, but you can't get the canonical ω without something like replacement on N.

2 days ago, by user21820

Wait my last sentence is not necessarily true. If you allow defining partial functions on the universe, you could define succ = ( type S ↦ S union {S} ), and then f = ( N n ↦ if n = 0 then {} else succ(f(n−1)) ) and then ω = { f(n) : n∈N }. The resulting ω that you get may not be as useful as you think.

2 days ago, by user21820

Notice that the ability to define partial functions and the last step are a bit like having replacement on N, which can be sort of justified by noting that we don't assume f is a total function at the start, but can prove by induction that it is, and hence the range of f makes sense.

In contrast, we can easily construct rather long non-canonical well-orderings without any kind of replacement, and show that their 'equivalence class' belongs to WO.

8:29 AM

Just want to check if I understood something correctly, is ω = { f(n) : n∈N } contains all f(n) where n range through all the naturals, or only some of them because f is not a total function?

As in my second quoted comment, it is philosophically justifiable to use induction to prove that f is total.

So ω defined as { f(n) : n∈N } would indeed contain f(n) for every natural n.

But if N is infinite, the usual induction will never enumerate all n in N (since each step we only prove some finite n is true) unless an induction axiom is used which guarentee that if the inductive case holds, then the case holds for the whole inductive structure in general (but again I am not very good at inductive types yet, perhaps that axiom is already included as part of the definition of an inductive type)

@Secret Induction is more of a meta-logical principle. Whenever I say induction I refer to at least the full schema.

Ah right, then it makes sense

Namely, we have the rule P(0) ∧ ∀n∈N ( P(n)⇒P(n+1) ) |− ∀n∈N ( P(n) ) for every property P on N.

In this case, the property would be that f(n) is a type.

This goes quite close to the edge, because for it to work we need to have "type" itself as an internal notion.

We could treat it as a definable concept (even though it's never defined).

8:38 AM

yes, that's called an induction axiom schema in set theory and also in second order arithmetic.

Btw since we can show f is total with the induction axiom schema, if we take f=id where id is the identity function, then the resulting term ω = { n : n∈N } will be like our usual von neumman omega (except not being a transitive structure, but that's ok because the ordering is still preserved like that in von neumman ordinals), thus it could still be useful

One thing that I am always wondering about ordinals is whether we can still define transfinite induction by having non von neumman ordinals that has an ordering isomorphic to the von neumman ordinals, but not under $\in$

We also have another issue to deal with if we use 3-valued logic. The implication in the induction rule can't be Kleene's implication if we want it to be able to handle properties that may be null. If so, then we can also write the rule as an axiom schema. If not, then what I wrote is 'better' as we wouldn't assume LEM. In other words, "S is a type" could be true/false/null.

@Secret We definitely can do this, which is compatible with reasoning about WO.

But not ORD.

@user21820 I am not sure if I understood this properly. If f is something obvious like the identity function, then I think the induction rule will not end up with null values, but if f is something more complex, then I agree the null case will arise and thus the induction rule will not be total and hence cannot be an axiom schema

so I guess we will be ok at least for ω. Anything larger, I am not sure yet

so yes, the induction rule you wrote will allow us to handle the null case because then ⇒ will be Kleene's implication

8:56 AM

@Secret It's not the problem with f. It's the problem with P.

You need P(n) to be "f(n) is a type" for the construction of ω as a canonical ordinal.

I see, so I think ω should be ok because the naturals n will be a type since we construct them as an inductive type, but anything somewhere beyond ω, then "f(n) is a type" may be null

Uh you don't get the point... Look at the definition of f again. It is not clear that "f(n) is a type" is always true or false.

Is it possible for "id(n) is a type" to be null?

I agree that for generic f the possiblity for a null value is likely, but I am not very sure whether id will also suffer this problem

in particular, id(m) where m is nat should also be nat

@Secret There is no problem for id, but it's the wrong question. The point is that if you want the canonical ordinal for ω, you'd have to use the f that I defined, for which it isn't possible (without induction) to determine that f(n) is always a type. In general, you can't assume that "S is a type" satisfies LEM, and so you would have to justify it directly.

For natural n, you would have id(n) = n, and if your intended world is a syntactic one, you could presume that you can distinguish types from naturals.

So if you have such a presumption then yes "id(n) is a type" would be a simple "false" for every natural n.

but the naturals in type theory are commonly defined as an inductive type, so I don't see any reason why they cannot be a type

9:06 AM

I didn't say that. You need to read my statements carefully.

First read the quoted comments again for the particular definition of f that I am talking about, and tell me if you think it's obvious that "f(n) is a type" is true or false (without using induction).

> succ = ( type S ↦ S union {S} ), and then f = ( N n ↦ if n = 0 then {} else succ(f(n−1)) ) and then ω = { f(n) : n∈N }

Computing...

succ : type n ↦ n union {n}
f(0) = {}
f(1) = succ(f(0)) = 0 union {0}
f(2) = succ(f(1)) = 0 union {0} union {0 union {0}}
...

ω = { f(n) : n∈N }

hmm...

the term e.g. 0 union {0} union {0 union {0}} looks nothing like the naturals

@user21820 is that what you mean by "f(n) is a type" may be null?

sorry typo

f(0) = {}
f(1) = succ(f(0)) = {} union {{}}
f(2) = succ(f(1)) = {} union {{}} union {{} union {{}}}

9:26 AM

in Mathematics, 5 mins ago, by Secret

Is it possible to define transfinite induction without using heredity transitive sets. That is, does there exists a structure with an ordering isomorphic to the ordinals but without the property of being heredity transitive?

in Mathematics, 4 mins ago, by Secret

One thing I never understood about "Ordered under $\in$" is why we are doing that besides the reason that the will ensure every number can be written as a set and limit ordinals can be wrote in terms of unions

in Mathematics, 1 min ago, by Secret

I am fine having all my structures not ordered under $\in$ if there is somehow a way to reproduce the well ordering of the ordinals, but throwing away the requirement of "under $\in$". Probably set theory just cannot do that job for me. I need something more expressive such as type theory

In short, I am not interested in reproducing the canonical ordinals/von neumann ordinals. I just want something that reproduce the well ordering of the ordinals and all its arithmetical and fixed point properties without the notion of membership so I can do transfinite induction

More precisely, I want to produce the transfinite sequence:

0<1<2<3<4<...< ω < ...

but I don't need $0 \in 1 \in 2 \in 3 \in ... \in ω \in ...$

[Example experiment during downtime]

Type nat

0 : nat

@Secret I don't think you understand the von Neumann ordinals, and that is why you didn't understand my definition.

If you just have well-orderings, then you cannot have certain properties of the canonical ordinals, such as the union of any set of ordinals is an ordinal.

@Secret As I said earlier, you can simply use any syntactic representation and be able to define rather long well-orderings.

The problem is that your well-orderings are not going to be as useful. You said you want to do transfinite induction, but typically the only significant use of that is uncountable transfinite induction.

I'm not aware of any other significant use of transfinite induction in modern mathematics.

Simply because ordinary induction on naturals is enough for practical mathematics.

But just to make sure you understand conventional ZF ordinals, you should probably revise them:

2

A: Definition of Ordinals in Set Theory in Layman Terms

Counting has two purposes, namely for specifying sizes and indices. These are directly related for finite quantities, because the number of natural numbers (including $0$) less than $n$ (before the position $n$) is $n$. But in set theory, when generalizing to infinite sets these two notions becom...

@Secret <− In particular you will see that there is more than just those properties of canonical ordinals. For example the class ORD is transitive and well-ordered under ∈ and hence cannot be a set. You clearly don't get this with WO.

Also you get transfinite induction on ORD for any definable property, not just induction up to any canonical ordinal.

Since I'm of the predicative viewpoint, I of course do not find any of this to be compellingly meaningful, but I'm just stating them for you to get an idea of why set theorists like canonical ordinals.

9:52 AM

Let me read and revise this before continue. I think one reason I am not aware of the many nice things about von neumann ordinals is I usually focus on the structures and properties of the ordinals themselves, and not much about their logical properties.

That is, given a mathematical object, I am usually more interested in the object itself before thinking about how it is used in other areas, which also explained why back in a very long time ago I found hard to understand induction schema since it is about how the object I am interested in is used in other areas, but not so much about the…

@Secret Yes go ahead and read that post first. Though as I said, you should find that from a predicative viewpoint an abstract notion of ordinals is not even needed at all, since in practical mathematics we don't have need for uncountable sequences.

It's just like computable ordinals. For any particular application, it may be convenient to construct some fixed computable ordinal. But I don't know of any practical need for the whole 'sequence' of computable ordinals, and predicatively we can't obtain such a thing.

10:22 AM

.
QUOTE: Now the next natural step is to find a canonical form for well-orders, which we shall call ordinals. Take any well-order XX. Recursively define the sequence ff on XX by f(i)={f(j):j∈X<i}f(i)={f(j):j∈X<i} for each i∈Xi∈X. Then its range {f(i):i∈X}{f(i):i∈X} ordered under set membership ∈∈ is isomorphic to XX! (Exercise: Prove this by using transfinite induction to prove simultaneously that {f(j):j∈X≤i}{f(j):j∈X≤i} and f(i)f(i) are well-ordered under ∈∈ for every ii in XX.) We use this well-ordering as the (canonical) ordinal for XX, which we shall denote by ord(X)ord(X). We will als…

ok I guess my confusions might be because I am fooled by intuition again. Let me explain why:

If I give you the following list of numbers
$$0,1,2,3,4,5,6,7,8,9,10$$
and ask you to pick e.g. 6, then you can circle out 6 without need to said anything about other numbers

However, if you are a computer, you need to first count from 0 to 5 before reaching 6, therefore to specify where 6 is, you need to specify it is the number after 0,1,2,3,4,5

More generally in recursive definition, as you outlined in your MSE:

$$f(i)=\{f(j):j\in X<i\} \text{ for each } i\in X$$

and it is this type of nesting in the definition of recursive definition that motivate us to define canonical ordinals as heredity transitive sets and hence von neumann ordinals

Yes that is the way I see it. Though Asaf said in a comment that he doesn't know what von Neumann's original motivation was.

@Secret And also note that this step needs replacement.

because $f$ may not be reifiable?

I didn't mean philosophically. I meant absolutely. That post was written from a ZF viewpoint, and that step requires the replacement schema. If you work in ZF−R, then you can't construct f in that step.

(In general, whenever you mentioned that something is impredicative, often my response is to try to look for the symbol that might have a null value, because it is easier for me to understand that way)

From my perspective, it's not clear that it should be predicative.

Will be away for a while.

10:33 AM

Hmm, so that means for any well ordered collection, even i I want to just pick one specific element, I cannot just circled it out directly and must specify where it is in relation to other elements. I always thought I can get away with that step

I always thought a well ordered collection will mean everything is laid out in discrete chunks on the table and I can easily pick any element I want because they are all uniquely labelled somewhat by the ordering

so I can just specify what label it is to pick it up

but it seems I cannot do that

11:00 AM

I think that it can be predicatively acceptable to construct f = ( j ↦ { f(j) : j ∈ X[<i] } ), but you cannot get LEM for "f(i) ∈ f(j)" for i,j ∈ X. If i < j then you can get f(i) ∈ f(j), but otherwise you may not be able to determine that f(i) is not a member of f(j) = { f(k) : k ∈ X[<j] }. So then { f(i) : i ∈ X } is not well-ordered under ∈, and so this construction is useless.

@Secret so you would rather we leave them unnamed?

yesterday, by user21820

@Secret I don't know what you're saying here and in your next 8 comments. Well-orderings come with a set and a binary operation. The well-ordering (1,0,3,2,5,4,...) is not the same as the well-ordering (0,1,2,3,4,5,...). Thus my comment shows predicatively that there are uncountably many distinct well-orderings.

@LeakyNun: See above and following comments for why you can show without doubt that there are uncountably many distinct well-orderings isomorphic to naturals.

@LeakyNun Not really, but like user21820 said, we need a more systematic way to extend special functions, otherwise we can go on and call any formula a special function and that will be too arbitrary

Btw the following thought process that occured before the final 3 posts in main and after "but I seemed cannot do that" may not make sense:

@user21820 ok understood

> Since in a well ordered set all elements are unique, linearly ordered and every subset has a minimum, won't the element themselves already serve as their own index since its positioning in the set is unique and thus in any induction that requires a specific element, we can pick out such element and use the element itself as an index and hence removing the need for ordinals as heredity transitive sets?

I think I need to reread the comments again, it seems I get confuzzled by something random in my thinking

11:09 AM

@Secret If you read my post slowly, you will see that that is exactly what happens in ZF already. You do not need canonical ordinals for induction along a particular well-ordering.

Of course, predicatively you need to also worry about what "subset" means.

But for countable well-orderings (the image of a function on naturals) that usually does not pose a problem.

> uncountably many distinct well-orderings isomorphic to naturals.

That's an ok fact for me, much better than having to deal with nested sets that makes my eyes bleed when looking at them. lol

@Secret Of course. I don't have a problem with that either. I'm just making the differences clear. The whole idea of attempting to collect isomorphic structures into a single class pervades mathematics, on the other hand.

{ Ø, {Ø}, {Ø, {Ø}}, {Ø, {Ø}, {Ø, {Ø}}} }

= my eye is bleeding

The axiom of infinity in ZF literally says that there is a set containing ∅ that is closed under successor...

Can you imagine the infinite-depth nesting?

That one is ok, since in each step there are only two "things" appearing: The object of interest and its sucessor. But somehow, laying it all out like above, and then my eyes started to bleed

meanwhile, the following looks less eyebleed to me:

Ø,{Ø},{{Ø}},{{{Ø}}},...

however it is obviously not heredity transitive

The reason it is easier to read the above is there's really only one kind of nesting

however, the following is not very different from (and I ran out of suitable sentences to fill in this blank) :

Ø = 0
{Ø} = 1
{{Ø}} = 2
...
(Ø,{Ø},{{Ø}},...) = $\omega$
(Ø,{Ø},{{Ø}},...), Ø = $\omega+1$
(Ø,{Ø},{{Ø}},...), Ø, {Ø} = $\omega+2$
...
(Ø,{Ø},{{Ø}},...),(Ø,{Ø},{{Ø}},...) = $\omega 2$
(Ø,{Ø},{{Ø}},...),(Ø,{Ø},{{Ø}},...),(Ø,{Ø},{{Ø}},...) = $\omega 3$
...
($\omega$,$\omega$,$\omega$,...) = $\omega^2$
($\omega$,$\omega$,$\omega$,...),($\omega$,$\omega$,$\omega$,...) =$\omega^3$!!!!

!Error, stackoverflow!
Ok this does not work

(I think I am rambling now, I need to sit down and re read everything)

perhaps now's time to do some chemistry to unknot my brain a bit

11:39 AM

Lol.

@Secret: Ok see you next time. Are you attending the incompleteness theorem discussion tomorrow?

Probably, let me check what that time is in sydney time

Hmm, 22:00-0:00 syd, should be possible since I don't need to go to uni early on monday

I really should be catching up on my research by programming that tedious calculation that replaces 11 templates, but I keep procrastinating to foundations of mathematics because it is less repetitive than coding some computer infrastructure needed to do my chemistry

@Secret: Haha.. go do some chemistry now? There is another user who is also in Australia, which is why I shifted the time back from the original 1am GMT.

« first day (29 days earlier) ← previous day next day → last day (470 days later) »

Transcript for

Oct '1721

$Mathematics$ Mathworks (Not the main chat!)

Maths department of SecretLabs SE Branch (chat.stackexchange.c...

join this room
about this room

00:00

06:00

12:00

18:00

all times are UTC

$Mathematics$

site design / logo © 2024 Stack Exchange Inc; legal

mobile