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& #39;s">https://www.math.uni-bielefeld.de/~sillke/N... talk about how primitive functions on β even get defined. I& #39;m using Terry Tao& #39;s Analysis I as a reference. 1/ https://twitter.com/kareem_carr/status/1293942267410108417">https://twitter.com/kareem_ca...
Let& #39;s">https://www.math.uni-bielefeld.de/~sillke/N... talk about how primitive functions on β even get defined. I& #39;m using Terry Tao& #39;s Analysis I as a reference. 1/ https://twitter.com/kareem_carr/status/1293942267410108417">https://twitter.com/kareem_ca...
β 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/
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& #39;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& #39;s really the same flavor of construction: we& #39;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/
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& #39;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/
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/
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