tirix
commented
3 months ago In my set.mm mathbox, I have a few theorems around ~df-sseq which allow to build functions based on strong recursion.
I used it for the Fibonacci sequence, which only requires access to the last two terms, but in principle you can access all terms in the sequence.
However this definition relies on Words and NN0, you might have wanted to avoid that.
Right now we have proofs for qnnen (equinumerosity of rational numbers and natural numbers) via the Schröder–Bernstein theorem (in set.mm), and via the constructive theorem that a mapping with the natural numbers exists if a set has decidable equality, is infinite, and is countable (in iset.mm).
Although there's no particular reason we need a more direct proof, I hadn't even seen any until now. If we want to formalize it we'd call it qnnenALT or some similar name.
See Tom Edgar's entry at https://aperiodical.com/2024/07/the-big-internet-math-off-2024-round-1-match-7/ proving qnnen via Stern’s diatomic sequence. Defining this sequence in metamath should be feasible using the given recursive definition (although it isn't the straightforward use of
seqwe are used to, as it requires access to all previous terms, not just the immediate predecessor).