Mathematicians who are finitists.

[polymath257]

Your ticket to fame, perhaps?  On the other hand, Mike Pence once said on the floor of the United States Senate that he believed that Science would someday vindicate ID.  "Someday" is, of course, a long, long time.

You make me sad.

Take the following primitive recursive function

x_0 = 1
x_{n+1} = 1 + 1 / (1 + x_n)

I claim that |x_n^2 - 2| <= 1/2^n. By induction:

Base case: |x_0^2 - 2| = 1 <= 1/1
Step case:

|x_{n+1}^2 - 2| = |(x_n^2 - 2) / (1 + x_n)^2| <= (1/2^n) / (1 + x_n)^2 < 1/2^{n+1}.

All the rational algebra here is finitistic.

Next, for any rational epsilon ε > 0, find the smallest power p of 2 such that 2^p > 1/ε. This can be found with another primitive recursive function. We then have

x_p^2 - 2 <= 1/2^p < ε.

After thinking a bit, this does not quite prove the convergence since you need to show that
|x_n^2 -2|<eps for ALL n>=p where p is that smallest exponent.

Is there a finitistic definition that gets around this issue?