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.
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 ...
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.
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.
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.
I think the traditional word for the "super-natural number" is "nonstandard integer".
You correctly notice that in case of nonstandard integer, the recursive definition alone is ambiguous, because while the standard integers are connected to zero by a finite chain of successor operations, the nonstandard integers are only chained to each other in infinite chains unconnected to zero. So you could have multiple implementations of a recursive function, each of them giving the same value for the standard integers, but different values for the nonstandard ones.
But there is one extra constraint that I think you didn't take into account. Peano axioms contain the "axiom of induction", which... if you look at it from a certain perspective, says: "whatever (first-order statement) is true for standard integers, it must also be true for nonstandard integers". Well, it doesn't say that directly; it's more like "whatever is true/false for some integers, there must be a smallest integer for which it is true/false".
This further constrains the possibilities for the "+" operation. If you can e.g. prove for the standard integers that "a+b = b+a", then according to this axiom, the same must also be true for nonstandard integers. So if "nonstandard + standard" is defined unambiguously, then so is also "standard + nonstandard".
But this still leaves some space for ambiguity in defining "nonstandard + nonstandard".
After reading it, I still don't understand why the hate for "multiplication as repeated addition" compared to the recursive formulation. For programming at least, iteration and recursion are functionally equivalent (or at least convertible to each other). What's "wrong" with respect to that formulation for math?
the other formulation of plus is "strict" in the 2nd argument, you need to evaluate P |b| times to get a natural number out to case on, prior to that, you have a function call
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.
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 ...
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.
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.
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.
I think the traditional word for the "super-natural number" is "nonstandard integer".
You correctly notice that in case of nonstandard integer, the recursive definition alone is ambiguous, because while the standard integers are connected to zero by a finite chain of successor operations, the nonstandard integers are only chained to each other in infinite chains unconnected to zero. So you could have multiple implementations of a recursive function, each of them giving the same value for the standard integers, but different values for the nonstandard ones.
But there is one extra constraint that I think you didn't take into account. Peano axioms contain the "axiom of induction", which... if you look at it from a certain perspective, says: "whatever (first-order statement) is true for standard integers, it must also be true for nonstandard integers". Well, it doesn't say that directly; it's more like "whatever is true/false for some integers, there must be a smallest integer for which it is true/false".
This further constrains the possibilities for the "+" operation. If you can e.g. prove for the standard integers that "a+b = b+a", then according to this axiom, the same must also be true for nonstandard integers. So if "nonstandard + standard" is defined unambiguously, then so is also "standard + nonstandard".
But this still leaves some space for ambiguity in defining "nonstandard + nonstandard".
I feel like we have some miscommunication. I'm referring to this list of axioms: https://mathworld.wolfram.com/PeanosAxioms.html
And I asked myself what happens if we do away with axiom number 5?
As for the nonstandard integers, I think that's a different thing.
There also is apparently already a concept in math named the supernatural numbers (aka Steinitz numbers) but those were not the ones I meant either.
After reading it, I still don't understand why the hate for "multiplication as repeated addition" compared to the recursive formulation. For programming at least, iteration and recursion are functionally equivalent (or at least convertible to each other). What's "wrong" with respect to that formulation for math?
Is there any notable difference between how it's presented in the post
> Thus, addition is a function P:NxN -> N such that for all numbers a, b,
> 1. P(a,0) = a
> 2. P(a,S(b)) = S(P(a,b))
And this alternate formulation?
1. P(a,0) = a
2. P(a,S(b)) = P(S(a),b)
Ie "decrease one from b and add it to a", instead of "decrease one from b and add it to the total".
you can notice a difference if you think about strict vs non-strict evaluation.
the first implementation can be more efficient for implementing isPositive
then and we can terminate right therethe other formulation of plus is "strict" in the 2nd argument, you need to evaluate P |b| times to get a natural number out to case on, prior to that, you have a function call