How multiplication is defined in Peano arithmetic
5 comments
·June 14, 2025nrds
GregarianChild
The "intersection of all sets such that" is not vague at all. It's perfectly formally defined in ZF* set theories. But it's impredicative. One of the guiding ideas behind type theories is to minimise impredicative constructions as much as possible. After all, impredicative definitions are circular ... Of course there is no free lunch and the power of impredicative constructions needs to be supplied in other ways in type theories ...
pengstrom
I think the fact that the initial _size_ of the recursion can be arbitrarily large is where infinity comes in. No matter your resources, there might be (must be?) a recision problem that's too large, that requires too many steps.
ysofunny
I think "recursion" simpy said, allows for algorithms which end as much as "not ending algorithms".
but in practice, an algorithm has gotta end, otherwise it's not very useful. I think some academics would go as far as insisting a function or process which never ends is not even a proper "algorithm"; but I digress.
recursion does allow us to "reach the infinite"; however, philosophically, we can only ever grasp the finite.
im3w1l
It's interesting to consider the possibilities that you have if the recursion axiom is removed. Call those numbers the super-natural numbers. Let's state the recursion axiom A, and remove it.
A: If K is a set such that: 0 is in K, and for every supernatural number n, n being in K implies that S(n) is in K, then K contains every super-natural number.
Without A, there may be a set S that contains 0 every successor of 0 (that is it contains all the natural numbers), but still does not contain every super-natural number. There are three possibilities: There may some copies of N (e.g. a 0' successors 1', 2' etc). There may be some copies of Z (there is an axiom that no number has 0 as a successor, but 0' could be preceeded by -1'). And there may be some copies of Z_k (e.g. 0' followed by 1' followed by 2' followed by 0' again). We could call every copy of N, Z or Z_k a "branch" of the supernaturals.
I say may, because the axioms leave it open, it could exist or could not exist.
Now what happens if you define addition with the supernatural numbers? Let a and b be supernatural numbers. We will use the regular definition
a+0 = a
a+S(b) = S(a+b)
What happpens when we do this?
First let n be a natural number. Due to the recursive property of natural numbers a+n=S^n(a). So we can add a supernatural number on the left side to a natural number on the right side just fine. But what if we have a proper supernatural number on the right side? The definition is completely silent on the matter. But could we find a valid extension?
Thinking about it a little bit I found that defining a+b=b (for any b that is not a natural number) will be a consistent (but perhaps not very interesting or useful) extension.
Notice that this definition will pick the branch of the result based on b, except in the case where b is natural. This is the not a coincidence, for if b is from a Z_k branch then the result must also be from a Z_k branch, as can be found by applying the successor k-times (it could I suppose in theory be from a different Z_k branch though).
E.g.
If b is from a Z_3 branch then b=S(S(S(b))) meaning a+b=a+S(S(S(b)))=S(a+S(S(b)))=S(S(a+S(b)))=S(S(S(a+b))) so a+b is also from a Z_3 branch.
The claims in this article, such as those suggesting recursion has something to do with the infinite, are all relative to the set-theoretic foundation. This is not essential.
In contrast, in the type theories behind proof assistants like Coq, Lean, and Agda, recursion is intimately tied to _finite_ structures. Instead of the vague "intersection of all sets such that" which we see in the article here, recursion is a well-defined computational process, and defined in a rather obvious way once you're familiar with the background.