In the words of Donald Knuth (on this very topic), "But no, no, ten thousand times no!" (source: https://www.math.uni-bielefeld.de/~sillke/NEWS/0-0.html)

Let's talk about how primitive functions on ℝ even get defined. I'm using Terry Tao's Analysis I as a reference. 1/ https://twitter.com/kareem_carr/status/1293942267410108417
ℝ is constructed step-by-step:
1. Obtain the naturals β„• somehow. Popular choices include (a) taking Peano axioms as fundamental, (b) using Zermelo-Frankel axioms to construct finite ordinals, (c) defining an inductive type, or (d) the classic, accepting β„• from God. (I kid.) 2/
2. Construct β„€ as a quotient of β„•Γ—β„•: specifically, pairs (a,b) where aβˆˆβ„• and bβˆˆβ„•, interpreted as purely formal expressions "a – b", with "a – b" and "c – d" considered equal iff a+d = c+b (where the + here is Peano addition, of type β„•Γ—β„•β†’β„•). 3/
3. Construct β„š as a subquotient of β„€Γ—β„€. This is very similar to step 2, where we "closed over" subtraction (which is not always defined on β„•, e.g. 2-5βˆ‰β„•), but now we close over division. We declare that "a / b" and "c / d" are equal iff aβ‹…d = cβ‹…b. 4/
(The only new hitch with division that wasn't a problem with subtraction is that if we allow all such formal divisions, every "rational" would equal "0 / 0" since 0β‹…d = 0 = cβ‹…0. So we restrict to the subset {(a,b) | aβˆˆβ„€ ∧ bβˆˆβ„€ ∧ bβ‰ 0} before taking the quotient.) 5/
4. Finally ℝ is defined as the Cauchy completion of β„š. This is quite a bit more complicated than closing over " – " or " / ", but it's really the same flavor of construction: we're closing over formal limits of Cauchy sequences, considering them elements of the new field ℝ. 6/
Now we have ℝ; how do we define operations of type ℝ×ℝ→ℝ? We recapitulate the construction of ℝ:
1. First we define the operation on β„•.
2. Then we extend to β„€ and show it respects equivalence.
3. Similarly, extend to β„š.
4. Finally, extend to formal limits, hence ℝ. 7/
Defining primitive operations on β„• from scratch is already a little challenging: β„• is infinite, so we can't just write down a function table. The only way is with an induction argument, or a recursive function (which are the same thing, via the Curry-Howard correspondence). 8/
In the case at hand, x^y, we start with xβˆˆβ„• and yβˆˆβ„•, proceeding by induction on y:
Base case. If y=0, x^y is defined as the multiplicative unit, 1.
Induction case. If y=succ(n), x^y is defined as xβ‹…(x^n).
(You might notice 0^0 is already determinate at this early stage!) 9/
Because the above definition makes use of x only as a multiplicand, and using a separate development of multiplication as a primitive (following the same pattern, β„•β‡’β„€β‡’β„šβ‡’β„), that exact same definition is still valid for xβˆˆβ„ and yβˆˆβ„•. Next we can generalize y. 10/
If yβˆˆβ„€ then either y equals a natural β€œn - 0” (in which case we use the previous definition) or y is the negative of a natural β€œ0 - n”, in which case if xβ‰ 0 we can declare x^y as the multiplicative inverse of x^n. 11/
For yβˆˆβ„š, we use the auxiliary notion of an nth root (for nβˆˆβ„•). When xβ‰₯0 the set {zβˆˆβ„ | zβ‰₯0 ∧ z^n≀x} is nonempty and bounded above. So the supremum of it exists, and we use this to define x^y when y = β€œ1 / n”. When y = β€œk / n”, x^y:=(x^k)^(1/n), and this respects =. 12/
Finally, for yα΅’βˆˆβ„š, if xβˆˆβ„ and x>0, it’s a theorem that if (yα΅’) is a Cauchy sequence, then (x^yα΅’) is also Cauchy, and its limit respects equivalence of real numbers, so we can extend to yβˆˆβ„ if x>0. 13/
To sum up, we have a well-defined value for x^y in the following cases:
1. xβˆˆβ„ and yβˆˆβ„•
2. xβˆˆβ„, xβ‰ 0, and yβˆˆβ„€
3. xβˆˆβ„, xβ‰₯0, and yβˆˆβ„š
4. xβˆˆβ„, x>0, and yβˆˆβ„
Each new case is a conservative extensionβ€”where the domains of definition overlap, the defined values agree. 14/
But the domains of definition are not strictly increasing. Indeed, 0^0 is not handled by case 2, nor case 4, but it is handled by case 1 & case 3. Confusion arises if we imagine that the limit-based case 4 is the final, most general definition because both x and y are in ℝ. 15/
Exponentiation at its core is a model of repeated multiplication, with its properties like x^(a+b) = x^aβ‹…x^b. Coherent extensions let us generalize this to expressions like e^Ο€. But if we end up *undefining* expressions defined in the simplest case, something went wrong! 16/16
You can follow @davidad.
Tip: mention @twtextapp on a Twitter thread with the keyword β€œunroll” to get a link to it.

Latest Threads Unrolled: