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

  • Not sure I understand the question, but are you by chance confusing "constructive" (provable with only constructive methods) with "computable" (derivable from a finite chain of inferences from the axioms)? There are lots of theorems that are computable but not constructive. Basically any theorem that uses the LEM or proof by contradiction is non-constructive. Apr 27, 2022 at 16:09
  • @DavidGudeman thanks, I added more hopefully its clearer.
    – J Kusin
    Apr 27, 2022 at 16:28


You must log in to answer this question.

Browse other questions tagged .