Back to Search
Start Over
Extracting Computable Bounds (and Algorithms) From Classical Existence Proofs: Girard Domains Enable Us to Go Beyond Local Compactness.
- Source :
-
International Journal of Intelligent Technologies & Applied Statistics . Jun2019, Vol. 12 Issue 2, p99-135. 37p. - Publication Year :
- 2019
-
Abstract
- In classical mathematics, the existence of a solution is of ten proven indirectly, nonconstructively, without an efficient method for constructing the corresponding object. In many cases, we can extract an algorithm from a classical proof, e.g., when an object is (nonconstructively) proven to be unique in a locally compact space (or when there are two such objects with a known lower bound on the distance between them). In many other practical situations, a (seemingly) natural formalization of the corresponding practical problem leads to a non-compact set. In this paper, we show that often, in such situations, we can extract efficient algorithms from classical proofs--if we explicitly take into account (implicit) knowledge about the situation. Specifically, we show that if we consistently apply Heisenberg's operationalism idea and define objects in terms of directly measurable quantities, then we get a Girard-domain type representation in which a natural topology is, in effect, compact--and thus, uniqueness implies computability. [ABSTRACT FROM AUTHOR]
- Subjects :
- *EVIDENCE
*ALGORITHMS
*MATHEMATICS
Subjects
Details
- Language :
- English
- ISSN :
- 19985010
- Volume :
- 12
- Issue :
- 2
- Database :
- Academic Search Index
- Journal :
- International Journal of Intelligent Technologies & Applied Statistics
- Publication Type :
- Academic Journal
- Accession number :
- 137788527
- Full Text :
- https://doi.org/10.6148/IJITAS.201906_12(2).0001