How should one think when reading the statement "Let x be any arbitrary ..."? Suppose in a proof there is a statement "Let $x$ be any arbitrary real number".
Semantically, I understand that this means "Consider for any (fixed) real number and
let us call that $x$ for the sake of referencing in the future".
However, I am not quite sure how should I think about the referenced object.

*

*Should one vaguely think of some real number in mind such as $0.031$ or $3145$, or $-3$ (And after the reasoning about that particular object is completed, in one's mind, they argue that the reasoning can be applied to any real number)?
Problems that occur to me:
If one has some specific number in mind, it seems to me that it will increase the probability that the reasoning will not be general, and one has to be aware of a corner case to be confident that they arrive at the generality. To me, this seems that there is a loss in the rigor of reasoning which decreases the degree of belief in the proposition being proved.


*Should one remain at a highly abstract level, i.e., treats it as some mathematical object that is in $\mathbb{R}$ without thinking about any specific number?
Problems that occur to me:
If one thinks about it very abstractly, to me, it is really difficult to reason about this abstract object, a proof will be unintuitive, and it takes a relatively long time to understand a proof. To me, this seems more rigorous but at the sacrifice of the enjoyment of doing mathematics  (The problem can be seen when reading "Let G be any graph" and not imagining any vertices and edges or reading "Let A be any matrix" and not imagining any specific dimension)
Or in the end, we cannot be sure of any proof we have done unless we prove them syntactically using rules in an axiom system like a game?
Do you have any insight/advice on how should one think/what should be going on in their brain regarding the issue? (Or do you have any recommendations of philosophy/logic books discussing the issue? I began reading Shoenfield's mathematical logic book a while ago but he states that the book studies logic syntactically, so I stopped since I am not sure whether the book will address this issue)
Thank you in advance!
 A: Since you're actually asking about the underlying logic, you should be aware that this is a common but misleading usage of the word "let". As explained here, there are many other phrases that can be and have been used for this purpose, and one of them is close enough to your attempt:
  Consider any real number $x$. Then [blah blah about $x$].
See this post for a Fitch-style deductive system for FOL, which would clarify the logical structure of proofs that you are looking for. In particular, "let" should be reserved for ∃elim. In contrast, what you want is ∀sub, which allows you to create a new subcontext $C$ in which some variable $x$ that is unused in the current context is bound within $C$, meaning that within $C$ you can refer to $x$ as an object of the specified type. For example:
  Given $x{∈}ℝ$:
    ...
    $x·x ≥ 0$.
  $∀x{∈}ℝ\ ( \ x·x ≥ 0 \ )$.
Of course, when doing mathematics, we usually cannot think totally abstractly, especially when in the process of finding a proof. So we do pick up some examples of real $x$ in trying to explore what we can hopefully can say about arbitrary $x$. However, once we think we have found a proof (maybe with the help of those examples), we still need to verify the deductive steps in the proof, and for that purpose of course the $x$ has to be completely abstracted.
You can think of the proof as a kind of program, where the subcontext specified by "Given $x{∈}ℝ$:" actually asks the user for an input $x$ that the user can justify is a member of $ℝ$, and the validity of the proof guarantees that the program never makes a false assertion. This viewpoint is related to game semantics, and provides something that is neither blind syntactic symbol-pushing or vague intuition.
