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.

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.

> 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".