[amavect]

My favorite math paper is "Is 10^10^10 a Finite Number?" by David van Dantzig. It lies more on the side of philosophy, so many can understand it easily. I first learned about it many years ago from Van Bendegem's list of strict finitism papers, and I would recommend that list for anyone interested in learning more about strict finitism.

For my personal opinion, strict finitism provides a richer field of study than potential infinitism or actual infinitism. Compare this to Errett Bishop's constructive analysis that requires the calculation of bounds to real numbers, instead of classical analysis only requiring that a real number exists. Much more difficult, though more precise.

I found "On Feasible Numbers" by Vladimir Sazonov to have application for computers. In a feasible mathematics, a large number fails to exist (say, 2^512), but a proof of contradiction must exceed such a large size (perhaps larger than the universe). Likewise, we have unix time that tries to count forever, so we should pick a storage size so large that counting exceeds the heat death of the universe. 10^100 years worth of Planck seconds fits in 501 bits, so round that to 512 bits. 512 bits of time ought to be enough for anybody :)

https://jeanpaulvanbendegem.be/home/papers/strict-finitism/

[rini17]

You know about busy beavers? These programs do fit in few bits, yet the number of states they can reach does not.

[amavect]

Of course, I follow the bbchallenge project. That's like the distinction between 2^32, 4294967296, and a string of tally marks that cannot fit in this comment. In a pithy way, strict finitists prefer numbers as tally marks. I find value in that perspective.

[jibal]

2^512 is the number of distinct values of 512 bits ... it sure seems to succeed in existing. SHA-512 is a cryptographic hash that depends on that.

[amavect]

2^512 exists in binary notation, but not in unary notation (tally marks, successor function). We conflate these ideas of "number", trying to forget the practical differences. Quite frustrating! SHA-512 depends on the fact that computers cannot feasibly increment to 2^512. A loop cannot feasibly run 2^512 times. Strict finitists emphasize those distinctions when they say 2^512 doesn't exist.

[jibal]

> 2^512 exists in binary notation, but not in unary notation (tally marks, successor function).

Sorry, but this is incoherent nonsense. The existence of a number doesn't depend on its representation ... but we can in fact represent any integer 0 <= n < 2^512 with 512 bits.

> SHA-512 depends on the fact that computers cannot feasibly increment to 2^512.

non sequitur

> A loop cannot feasibly run 2^512 times.

non sequitur

> Strict finitists emphasize those distinctions when they say 2^512 doesn't exist.

Cranks.

[amavect]

I don't mean to come off as a crank. I'd like to clarify the strict finitist position in a sensible way (what they mean is that 2^512 unary notation doesn't fit in this universe, and similarly 2^(2^512) in binary notation doesn't fit in this universe and thus "doesn't exist"), but clearly I fail at meeting your requirements, sorry.

[jibal]

Sigh. There was no mention of 2^(2^512),only the set [0, 2^512), each value of which can be represented with a different configuration of 512 bits in any computer (or storage medium) "in this universe". That these values cannot be enumerated within a small amount of time is completely irrelevant (other than that SHA-512 cannot be reversed in practice, which as I said is a non sequitur) ... 2^512 is quite finite, even for finitists.

And "doesn't fit in this universe" is unformalizable crank nonsense.

Over and out.

[amavect]

A few formalizations exist: bounded arithmetic, internal set theory, Nelson's predicative arithmetic.

From Buss's thesis "Bounded Arithmetic": "However, a recursive function may be computable only in a theoretical sense: the time required to compute it may be far larger than the lifespan of the universe. We are more interested in feasibly computable functions, which can be calculated by today's (or tomorrow's) computers."

And then he goes and defines an arithmetic hierarchy for polynomial functions.