The notion of scope as an integral part of mathematics is a particularly interesting suggestion. Mathematics is the study of abstract, quantitative truths (and falsehoods), and these truths, being universal, have universal scope (although you can constrain some truths as special cases of more general truths, but I doubt this is what the author had in mind). To consider this a problem indicates that the author is searching for a tool rather than a way of thinking.
The scope issue is not just for theorems. In programming, scope is about what meanings get bound to what symbols, whether those symbols are types, operators, data, etc. Even in math, we can see a notion of "binding" vs. "bound" vs. "free" occurrences of a symbol: seeing something like "∀x∈N.x+k≥0" would make me think "Ok, I see what `x' is, but what's this `k'?" Treating every definition like it's at top-level makes for unreadable code and unreadable math. Ever had to search back through a document looking for the definition of some notation only to find it buried in an earlier proof of an unrelated theorem without so much as a "Definition: …" marker? I would much prefer not to have to do that again.
Transferred to another domain, "Why should we need scope? What good would that do?" becomes "Why should pronouns have antecedents? What good would that do?" It is important to acknowledge that mathematical notation is also a tool for explaining the ideas one has discovered with it.
The scope issue is not just for theorems. In programming, scope is about what meanings get bound to what symbols, whether those symbols are types, operators, data, etc. Even in math, we can see a notion of "binding" vs. "bound" vs. "free" occurrences of a symbol: seeing something like "∀x∈N.x+k≥0" would make me think "Ok, I see what `x' is, but what's this `k'?" Treating every definition like it's at top-level makes for unreadable code and unreadable math. Ever had to search back through a document looking for the definition of some notation only to find it buried in an earlier proof of an unrelated theorem without so much as a "Definition: …" marker? I would much prefer not to have to do that again.
Transferred to another domain, "Why should we need scope? What good would that do?" becomes "Why should pronouns have antecedents? What good would that do?" It is important to acknowledge that mathematical notation is also a tool for explaining the ideas one has discovered with it.