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