@KennyLau That's why I said if it's too hard look at Hint 3+. It can be quite easily done in first-order once you see the hint.

@KennyLau I'm not familiar with the notation. Anyway there is an easier semantic approach using the BHK interpretation of provable sentences as programs that generate proofs. Recall that if you have A and ( A ⇒ false ), then you can apply the second to the output of the first to get a proof of false, and so you have a proof of ( ( A ⇒ false ) ⇒ false ). Thus given ( ( ( A ⇒ false ) ⇒ false ) ⇒ false ), then from A you can get ( ( A ⇒ false ) ⇒ false ) and then apply the given to get false.

Thus you have a program witnessing ( A ⇒ false ).

@Mathmore Oh no problem. This can always wait; you can deal with whatever you need to first. Later if you have questions about anything said earlier you can definitely ask. =)

@amWhy: Hello! Good to see you here. =)

@user21820 Can I do y=omega+x in first order zfc where x is natural?

@LeakyNun y not?

Are you asking what is the meaning of addition of ordinals?

Or whether it can be constructed in ZFC (yes it can).

@user21820 Good morning! (err, afternoon?, evening?)

@user21820 Check out my very recent Crude posts/comments.

@amWhy Is it 9am in the morning for you?

@user21820 No, but close to 8:00 am.

I see. You're up early. =)

@user21820 Yes, I've been up for three hours now! :)

@amWhy What... that's even before the birds get up, isn't it?

@user21820 but for arbitrary n?

could you guide me?

@user21820 at this point in time (October ! (argh!)), yes.

In a bit more than a month, we (central time US) go back to "standard time" so "5a.m." will become 4:00 a.m.

@LeakyNun I don't quite get the question then. If you have already defined addition of ordinals in ZFC, then of course you can construct ω+n for any natural n. Any object that is definable can be constructed. I think you're actually asking how to define addition of ordinals, rather than specifically about this particular sum.

@user21820 I can do omega+1 and omega+2 and omega+100

I just can’t do omega+n

[omega+100 is just omega+1+1+1...]

and n+1 is n U {n}

@amWhy I see.

@LeakyNun Okay so you're using the von Neumann ordinals.

Then what you need is the recursion theorem.

And unfortunately for you, since you decided to do this in ZF, you're in for a tedious business to prove the recursion theorem.

can i do that by hand?

It will not be much simpler to do that one instance.

hmm

I did {{{{{}}}}} before

someone guided me to do that by hand

would you know how to do that?

@LeakyNun I'm not sure what you mean. There is no way to do what you're asking for any recursive variant of ordinals, without the recursion theorem.

I’m just doing the natural numbers...

write a sentence such that p(5,{{{{{}}}}}) etc

I know that. If you go to the link I gave you, it's just for the recursion theorem for naturals.

@LeakyNun If you point me to the sentence for this, and the proof for it, then I could see whether it's correct or not. I don't see any reason it can be simpler than a proof of the recursion theorem.

chat search isn’t working

Anyway, I have to go now. I think that if you wish to work in ZF you should certainly know how the recursion theorem is proven in ZF since you need it for the construction of every recursive function.

ok

@LeakyNun Yes broken again. Never mind. Just take a look at the recursion theorem, which basically allows you to construct the recursive function f such that f(0) = ω and f(n+1) = f(n)⋃{f(n)} for every natural n.

I'll be back later.

p(x,y) := exists A [ (0,{}) in A & forall n forall p [ (n,p) in A -> (n+1,{p}) in A] & forall a foral b forall c [ (a,b) in A & (a,c) in A -> b=c ] & (x,y) in A]

@user21820 much like the godel coding of natural number sequences

@LeakyNun If that's what you wanted, you can easily do the same for von Neumann ordinals. However, this is not what is typically meant by constructing ω+n for arbitrary natural n, because that's just the first few steps in the proof of the recursion theorem, as you can see in my post. It doesn't produce a function, which is what you need to be able to use ω+n fully in other set-theoretic constructions.

@LeakyNun: And (for both variants) you will need the axiom schema of replacement, because here you don't yet have a set that serves as a codomain for the recursive function.

@user21820 I’m constructing the sentence to use replacement...

@LeakyNun The use of replacement comes when you have proven that for each function on [0..k] satisfying the recursion there is a unique function on [0..k+1] that satisfies the recursion. Functions on [0..k] are members of relations on N, so you have a first-order definable functional on a set, and can apply replacement to get its range and hence 'upgrade' from a functional to a function (relation between sets).

Anyway, did you finish the matching-brackets puzzle from yesterday?

But I'll be off soon so see you next time!

@user21820 isn't that bracket puzzle kind of like what we're doing now with sets?

@LeakyNun Yes but it's completely first-order in the language of strings with +, and the proof that it works definitely needs no replacement. Things are always hairy in ZFC when you deal with set-theoretic operations that invoke the powerset operation an unbounded number of times.

@user21820 we don't need replacement to do the set thing either?

I mean, my sentence is first order?

You forgot what I said above? Your 'solution' is not really a solution at all...

Just like you can say we can define Russell predicate by R(x) ≡ x∉x. Sure, R is a valid first-order predicate over ZFC, but it doesn't actually construct the set corresponding to it, so you can't use it like you can use other objects.

@user21820 did I say it constructs the set?

I just wanted a sentence p(x,y) that is true iff y={{{}}} [x-1 times]

@LeakyNun You didn't, which is why I said if that's all you wanted it's trivial to get one for von Neumann ordinals. You didn't respond to that. However, I keep saying that that's not the typical meaning that we convey when we say "construct in ZFC".

@user21820 why did I not?

is that sentence invalid?

or do I have to prove uniqueness?

@LeakyNun It's basically circular. You have a sentence that you intuitively think works. But you can't show that it works for all naturals without already having constructed the ordinals you want.

@user21820 which sentence are we referring to?

@LeakyNun <− This one.

$p(x,y) := \exists A [ (0,\varnothing) \in A \land \forall n \forall p [ (n,p) \in A \implies (n^+,\{p\}) \in A] \land \forall a \forall b \forall c [(a,b) \in A \land (a,c) \in A \implies b=c] \land (x,y) \in A]$

p(x,y) := ∃A [ (0,∅)∈A ∧ ∀n∀p [ (n,p)∈A⟹(n+,{p})∈A ] ∧ ∀a∀b∀c [ (a,b)∈A ∧ (a,c)∈A ⟹ b=c ] ∧ (x,y)∈A ]

The problem is that (I'm quite sure) if you don't use replacement, you will not be able to construct Zermelo's ordinals (the one your sentence works for) nor von Neumann's ordinals, so you'll be unable to prove that your sentence works at all, simply because you can't even express over ZFC what it means for the sentence to work.

You can prove specific instances to hold without using replacement. You can prove p(3,{{{}}}), because you can invoke the powerset axiom 3 times in your proof.

powerset axiom?

What you can't do is to construct the very ordinals which you set out to identify...

@LeakyNun Uh? How else do you construct {{{}}}??

@user21820 pairing axiom twice

are you saying that I cannot prove $\forall x \in \Bbb N \exists! y ~ p(x,y)$?

@LeakyNun Okay same result. You need to apply whichever axiom more and more times for each of those ordinals.

@LeakyNun You can, but you can't get the ordinals in a set without replacement, which is the whole point. If you don't, then we typically don't say that they are constructed in ZFC.

I don't know why you sometimes keep repeating yourself without reading my comments carefully.

what do you mean "get the ordinals in a set"?

This is like the third time I'm saying. Just like Russell's predicate R is definable but not constructible as a set, The set of ordinals { ω+n : n∈N } is constructible only via replacement.

the axiom schema of replacement writes $[\forall x \exists!y ~p(x,y)] \implies \forall u \exists v \forall r[r \in v \iff \exists s [s \in u \land p(s,r)]]$

@user21820 that's also the third time I'm saying that I'm not trying to construct that set!

I'll just quote myself:

p(x,y) := ∃A [ (0,ω)∈A ∧ ∀n∀p [ (n,p)∈A⟹(n∪{n},p∪{p})∈A ] ∧ ∀a∀b∀c [ (a,b)∈A ∧ (a,c)∈A ⟹ b=c ] ∧ (x,y)∈A ]

ok, so this is my proposed sentence to construct { ω+n : n∈N }

Either the question you asked is trivial because you already could do it for Zermelo's ordinals, or it is non-trivial if you want to construct the ordinals in the typical sense that logicians mean when they say "construct".

@LeakyNun This merely defines the relation, not construct the set. You use replacement in the manner stated earlier to get the set.

@user21820 do I use replacement with this sentence?

No you can't. As you asked earlier you need to prove the uniqueness before you can apply replacement.

can I prove uniqueness with this sentence?

@LeakyNun That's precisely why I brought up the recursion theorem, so that you just have to do the proof once instead of repeating it over and over for every recursive construction you want to do.

Not only that, the proof is cleaner without being cluttered by the specifics of this recursion.

hmm

could I ask another question?

Sure. Please understand that I say all the above because if you wish to work in ZFC you must pay attention to what can be defined and what is a set. There are many definable things that cannot correspond to sets.

alright

1. in NBG does the class {x|x∉x} exist? is it empty? is it a proper class?

2. in ZFC how do you construct ω1 i.e. the set of all countable ordinals?

wait I think I know the answer to 2 already

please answer 1 while I propose an answer to 2

to construct ω1, you take N and consider all possible well-orders upon N

a well-order is just an ordering on N

and an ordering is just a relation

which is just an element of the powerset of NxN

@LeakyNun Your answer is right.

@user21820 thanks

I believe in the finite version of NBG you take the class [∈] and [=] and intersect them and then complement

where [∈] is the class { (x,y) | x∈y } and [=] is the class { (x,y) | x=y }

wait, but their intersection is empty [because there is no set x such that x∈x, by regularity]

so their complement is V

so it is a proper class.

I've just answered my own questions, twice.

Correct as well. I was just going to say the same. Next time you can ask yourself first, since you type faster. =)

lolllll

Anyway ok I'm going off for real. See you next time!

bye