For the problems which can’t modified into a constructive proof, is there some useful notion of proving them to some computational approximation?
I’m referencing:
“Interpretations come at a cost: for example, when we pass from our initial, natural interpretation of P∨Q P ∨ Q to the unrestricted use of the idealistic one, ¬(¬P∧¬Q) ¬ ( ¬ P ∧ ¬ Q ) , the resulting mathematics cannot generally be interpreted within computational models such as recursive function theory ”
“because the computer can handle real numbers only by means of finite rational approximations, we have the problem of underflow, in which a sufficiently small positive number can be misread as 0 by the computer; so there cannot be a decision procedure that justifies the statement (). In other words, we cannot expect () to hold under our natural computational interpretation of the quantifier ∀ ∀ and the connective ∨ ∨ .”
So for non-constructive there is no “decision procedure”, but isn’t the second quote saying we can approximate better and better with a program that doesn’t halt. Like the algorithm which computes sqrt2 decimals we run for 100 trillion digits without halting. So we say this is a non-constructive version of sqrt2 is irrational because even without a decision procedure (program would halt), there’s still limitless precision. It isn’t constructive because it doesn’t give sqrt2 perfectly, but yet maybe 100 trillion digits is a proof? Anywhere else (science) that is called “proof”. We never have perfect accuracy except things like constructive math. Philosophically why is proof restricted for non-constructive math but not science?
Is there some opinion that this should be acceptable for mathematical proof? Is this method accepted under non-constructive math? Is it a different sect entirely and does it exist.
from https://plato.stanford.edu/entries/mathematics-constructive/.
Edit: Added Detail
