>>12533786 (cont)>phantom of transparencyIf you have read Girard, you should be able to understand where I'm getting at.
Girard, while more on point than other philosophers, jumps from a dead-end to another with his quantum-inspired derealism. All that he says about subjects (us) is absolutely right, but the object (the world) does exist indipendently from us, after all. We are limited in probing it, we don't have transparency, and to pretend otherwise makes us hallucinate "phantoms" (the Platonic realm, infinity, ...). This is the sign of a leaky abstraction, that the abstraction is not doing what it is saying it is doing. Then what is it doing?
Girard recognizes the importance of cut-elimination, that guarantees that the symbolic manipulation instructed by logical implication terminates.
No mathematics is truly infinite, because no mathematician died evaluating a proof, leaving to his successor to keep it going to check whether it terminates. All proofs are either instructions for finite manipulations or erroneous.
They are all finite objects with finite behaviour, and so are mathematical systems that describe any "infinite object", whose meaning is in the computation performed.
The monstruous objects Girard laments, such as the graph of a function {(x,f(x)} on an infinite domain, cannot exist, but what can exist is the instruction to compute such function f(x) on any potential element.
But now that you know how the function f can exist, you know how to interpret the meaning of the ramblings of the infinitist: when he says that he "actually has" an infinite set {(x,f(x)}, he's saying he has a function and can construct the pair (x,f(x)) at will, ignoring potentiality. That abstraction will leak and has been leaking for a century.
But all abstraction is leaky, non-halting computation, as you implied, is non-instantiable: in practice, we will check for finitely many, but arbitrarily high, steps whether it halts and then give up if it doesn't.
