3 ms·
> The only way to define non-computable things is to use excluded middle or choice. There is no other way. At least not in the underlying type theories of proof
by kd0amg 5y ago
> The only way to define non-computable things is to use excluded middle or choice. There is no other way. At least not in the underlying type theories of proof assistants such as NuPrl, Coq, Agda and Lean.
Meanwhile, ACL2 has the excluded middle and can still prohibit defining non-computable things. It needs termination analysis in order to do so, but these type theories rely on that too. Is the forgoing the excluded middle really gaining you the guarantee of computability?
- fmihaila 5y ago> Is the forgoing the excluded middle really gaining you the guarantee of computability? It doesn't follow; that uncomputable things cannot be expressed in a constructive system doesn't mean that everything that is computable in principle is also computable, or even definable, in that system (unless by "guaranteeing computability" you meant something else).