Some mathematical formulas directly suggest an algorithm for computing it (even if sometimes an inefficient one). For example, if we recursively define $\sum_{i=1}^nx_i=x_n+\sum_{i=1}^{n-1}x_i$, then this directly suggests a recursive algorithm for computing the sum. In fact we might even have a functional programming language where this is a valid program.

But some mathematical formulas are not even decidable, let alone suggest a specific algorithm for deciding it. For example, let $X$ be an uncountable set and $T\subseteq \mathcal P(X)$ an uncountable set. Then for example the property $\phi:\forall A_1,A_2 \in T, A_1\cap A_2 \in T$ is in general undecidable because the sets are uncountable, so we cannot check this for all sets $A_1,A_2$ (note this is a proporerty for $T$ to be a topology). However, we can imagine checking this with a hypercomputer: Execute a thread for each pair $A_1,A_2$, and check if $A_1\cap A_2\in T$. This will be an uncountable number of parallel threads. Then take an uncountable AND between the results of these threads.

Note that this is a "natural" algorithm, in the sense that we didn't make any specific implementation decisions.

Can we generalize this? I.e.

  • Is it possible, within some formal language for mathematics (e.g. calculus of constructions/calculus of inductive constructions) that can define any mathematical objects, to define a semantics for any mathematical formula that may use some form of hypercomputation to compute that formula?

  • Is there a name for this idea so that I can look it up?

  • $\begingroup$ I'm not exactly sure what you're asking but I believe the keyword you're looking for is 'oracle', e.g. oracle machine. $\endgroup$ – orlp Mar 11 at 21:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.