Thread by @davidad, In the words of Donald Knuth (on this very topic), "But no, [...]

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

Latest Threads Unrolled: