Hmm...

$\langle \underbrace{0}_{1\text{ term}},\underbrace{0,1}_{2\text{ terms}},\underbrace{0,1,2}_{3\text{ terms}},\underbrace{0,1,2,3}_{4\text{ terms}},\underbrace{0,1,2,3,4}_{5\text{ terms}},\dots\rangle$

$\exists Y \subset \Bbb{N} \forall (x\in \Bbb{N}) [\forall z [z \leq x \land ...]]$

ugh, this is much harder to wrote in logical terms than I thought...

@Secret Heh. Well I don't particularly fancy making things unnecessarily complicated. There are a couple of easy ways to express this sequence via program-like constructs. Say python:

yeah I know I can use e.g. a for loop for that, but I don't know if there's a logic equivalent to a for loop statement

You will need recursion, which you can get via Godel's coding trick if you want to express it in an arithmetical sentence.

If you want to work in a system like ZFC, you also need recursion, which you can get via the recursion theorem. See sketch here. I had a much longer discussion with that user in this chat-room, which you can probably find by searching for "recursion theorem".

Something inspired from python: I wonder if the significance of the collection of natural numbers is that they form the simplest iterator to run a recursive algorithm

if a foundation has only induction, but lacking natural numbers (or any well ordering), I will imagine it will be quite hard to wrote a program in it

Perhaps, the above is me trying to understand the philosophical significance of arithmetic, and as we knew, it is often given by the Peano axioms

@Secret No you got it backwards again. We 'know' properties of natural numbers only because they seem to be relevant to describing the real world, nothing more than that.

We developed digital electronics and algorithms only because of that too, because (human-scale) finite binary strings are encodable in physical media.

If the real-world didn't have those properties, we wouldn't even be talking about natural numbers or algorithms.

@Nathaniel: Hello! Do you have anything you'd like to inquire about or discuss?

Ah, I was mostly just lurking and catching up on the discussion - I'd left this open in another tab, so if it said I was logged in for ages, that's why!

Though actually, I guess there's a couple of things I'm curious about regarding your answer at math.stackexchange.com/a/2677474/27193, and comments on that page. Not sure if I should post about them there or here.

@Nathaniel Feel free to continue here if you suspect it would be a long conversation.

And here would be more informal, of course.