Are professional mathematicians concerned with formalizing infinitely many dependent choices?

I've noticed certain arguments in analysis textbooks which rely on the principle of being able to pick elements infinitely many times. For example, an argument might go "Pick $x_1\in S$ such that $P(x_1)$. Having picked $x_1,x_2,\dots,x_k\in S$, pick $x_{k+1}$ such that $P(x_{k+1})$. This justifies the existence of a sequence in $S$ having properties X, Y, and Z." But this is not entirely induction; this is also recursion (and in some cases AC is used). And the recursion theorem/AC are totally absent from most textbooks. So how is this mathematical argument justified? Why doesn't the writer care about being explicit with the principles being used?

When I was an undergrad, this gave me anxiety.

This is basically a long comment: The thing is that when we construct sequences in the manner you described ("Having picked $x_1,x_2,\ldots,x_n\in S$, pick $x_{k+1}$,...") is much simpler to grasp than trying to make every single statement formal. Basically we are using the following theorem (or some suitable variant):

"Let $P(F)$ be a property about finite sequences. Suppose that there exists $x$ such that $P(x)$ holds and such that for every finite sequence $(x_1,\ldots,x_k)$ for which $P(x_1,\ldots,x_k)$ holds, there exists $y$ for which $P(x_1,\ldots,x_k,y)$ holds. Then there exists an infinite sequence $(x_1,x_2,\ldots)$ for which $P(x_1,\ldots,x_k)$ holds for every $k$".

The proof of this can be left as an exercise for anyone who is advanced enough to care about this, and as far as I know depends on the Axiom of Choice. It can be done as follows (no reference): Say we are working with real numbers. Recall that a finite sequence is simply a function $f:\left\{1,\ldots,N\right\}\to\mathbb{R}$, and an infinite sequence is a function $f:\mathbb{N}\to\mathbb{R}$.

Let $\mathcal{P}$ be the set of finite or infinite sequences $f:dom(f)\to \mathbb{R}$ for which, for each $N\in A$ $P(f(1),\ldots,f(N))$ is true. Then $\mathcal{P}$ is nonempty ($\mathcal{P}$ contains a singleton sequence, by hypothesis). We need to show that $\mathcal{P}$ has some infinite sequence. Order $\mathcal{P}$ by extension of functions/inclusion of graphs: $f\leq g$ iff $dom(f)\subseteq dom(g)$ and $g|_{dom(f)}=f$. Show that every totally ordered subset of $\mathcal{P}$ has an upper bound (exercise). So $\mathcal{P}$ has a maximal element $f$ by Zorn's Lemma/Axiom of Choice. Show that $f$ is an infinite sequence (exercise). We are done. QED

This is one of the things some people would call "part of the folklore". Something that basically everybody knows but noone took the time to write or really care about the details.

I tend to disagree with Luiz Cordeiro's answer.

I think the real reason why it appears that "no one cares" about this kind of thing is because the existing system of rewards and incentives in professional mathematics tend to confer an advantage upon one type of mathematician at the expense of the other.

Lets distinguish two kinds of mathematicians:

• Type A mathematicians are pragmatic; they focus on developing new techniques and machinery, and above all, on solving problems. They "get the job done", but they also make more mistakes and publish more false results, owing to less emphasis on formalization and rigor.

• Type B mathematicians are idealistic; they're primarily interested interested in rigor, clarity of thought, and the consolidation, formalization and unification of existing material. They don't produce as many new results as Type A mathematicians, but what they do produce is very carefully thought out, and more likely to stand the test of time.

Of course, this is an oversimplification: I'll get to that. But at this point, I want to try answering your question. My opinion is that the existing system of rewards and incentives confers an advantage upon Type A mathematicians, at the expense of Type B mathematicians. For example, Type A undergraduates tend to learn the material faster, because they're more open to doing things the lecturer's way, which they consider "rigorous enough." On the other hand, Type B undergraduates take longer to learn the material, because they fight it tooth-and-nail, spend a lot of time (rightly or wrongly) trying to fix what are perceived as half-baked arguments, and this makes their overall mark lower. However, these same students, if they make it far enough, are the one's who end up writing that textbook that ends up becoming the de facto choice in the field, because they've spent so long wrestling with every inch of the material, their understanding of its deeper structure ends up being rather highly developed. And, like I said, the ideas of Type B mathematicians are more likely to stand the test of time.

Anyway, long story short, I think that Type A students are more likely to go on to become professional mathematicians, while Type B students are more likely to drop out after (or during) their Masters or PhD programs, and often harbor no small level of resentment toward the mathematical establishment by this point. But putting the psychology of it aside, my point is really that lots of would-be mathematicians care (or cared) very deeply about rigor and formalization, but they were selected out by the "math selection filter," and this creates the sense that nobody cares about formalization, when the reality is much more complicated.

Perhaps this is why those people who contributed to the formalization of mathematics historically also tended to be smart: if you're concerned with formality, getting through the math selection filter is much harder, but raw brain power can help.

Now, for a bit of advice. Supposing you're a Type B student. You want to become a successful Type B mathematician, but the education system seems to be working against you. And you don't have the raw CPU cycles of greats like Alfred Tarski and Kurt Godel. Nonetheless, my thinking is that you can still succeed. The thing is, the Type A/Type B distinction an oversimplification. There's a middle ground, occupied by people I'd call "theory builders." These guys definitely care about rigor, but they also won't let the inability to make things quite as precise or perfect as they'd wish stop them from doing their work, because they're building a theory that's meant to be used by real people (usually Type A mathematicians or other theory builders) to solve real problems, and this helps them put their need for rigor on the back-burner temporarily in order to produce actual publishable papers and contribute to mathematics in the short term.

My thinking is that once you have enough "street-cred" from theory building, you can move more toward the formalization/rigor side of things, because at this point there's less pressure to publish. There's a time for letting your inner Type B mathematician off the leash, but you need to already have a career first.

This advice is completely hypocritical, by the way, because personally, my inner Type B mathematician pretty much dictates my thoughts and behavior. But that doesn't mean this works. I don't recommend being like me; my academic life is far too hard. Be a theory-builder, at least until you're established in your field.