Terminability of an algorithm and existence of an infinite sequence

Question

It is perfectly clear that when the familiar Gram-Schmidt algorithm is performed on a finite set of linearly independent vectors, the algorithm terminates and we get an orthogonal set of vectors. Fine.

Now they apply the algorithm to a countable set of linearly independent vectors in a Hilbert space recursively and get a countable orthogonal set of vectors. But the problem here is that this algorithm will never terminate, hence we cannot get the truly infinite collection of orthogonal vectors in finite time.

And now that I think about it, for any sequence that is defined via recursive relation (e.g. Fibonacci sequence), we shouldn't be able to write down a formal generating function because we don't have the truly infinite sequence!

So my question is: Does there exist an axiom in ZFC that allows me to say that there is truly an infinite collection satisfying the recursive relation?

Answer 1

$\mathsf{ZFC}$ set theory proves the following theorem:

Let $X$ be a set, let $X^{<\omega}$ denote the set of all finite sequences of elements of $X$ , let $[n]$ denote $\{0,1,2,…,n-1\}$ for $n\in \omega$. Suppose $g:X^{<\omega}\to X$ then there exists a unique function $f:\omega \to X$ such that $f(n)=g(f\restriction [n])$ for all $n \in \omega $.

Defining $g:\mathbb{N}^{<\omega}\to \mathbb{N}$ as $0$ for sequences of length $0$, $1$ for sequences of length $1$, and $\sigma(n-1)+\sigma(n-2)$ for sequences, $\sigma$, of length $>2$. One gets that $f$ is the fibonacci sequence.

One can prove the theorem by building partial approximations and then gluing them up together to form a single function. Details can be found in any set theory book, e.g. Jech-Hrbáček, under the name of the "recursion theorem".

Infact $\mathsf{ZFC}$ can prove much stronger versions of this theorem, again details can be found in any introductory axiomatic set-theory book.