Note: I am interpreting “algorithms” broadly, to include algorithms that require an infinite and even uncountable number of computational steps.

It seems to me that any definition can be seen as a specification of an algorithm in this sense: For example, consider the definition:

$$X=\{x:\mathbb R| \chi(x) \}$$

This specifies an algorithm: Check for each $x\in \mathbb R$ whether the property $\chi(x)$ is satisfied. If it is, add $x$ to the set $X$.

Question: Can we see all mathematical concepts as specifications of algorithms (possibly requiring uncountable computational steps)? Is there some kind of theory that formalizes this idea?

Why am I asking this? Because it seems to me that if this is true, then this suggests to me a deeper connection between math and computer science than I thought:

  • very eye-squinty: computer science treats the intension of concepts, and math treats the extension of concepts.

  • whether something is “computable” simply means whether there is a finite algorithm for it. Everything is computable in an infinite sense.

  • We can think of all of math in computational terms, even in uncountable contexts

  • Theorems about connections between different areas of math become theories stating that two different (possibly uncountable) algorithms produce the same output.

  • The difference between classical vs constructive logic and math, is that classical math allows for infinite/uncountable algorithms.

  • $\begingroup$ You seem to be conflating constructivism with finitism. The two are not synonymous: constructivism does not necessarily involve finitism. For example, IZF and CZF include the Axiom of Infinity. I get the impression you might also think that 'countable' = 'finite' and 'uncountable' = 'infinite'? If so, that's not the case: the former means 'countable infinity', the latter 'uncountable infinity'. $\endgroup$ – Alexis Mar 4 at 0:11
  • $\begingroup$ @Alexis, “countable” in my terminology means either finite or countably infinite. Uncountable means what you mean. I might be conflating constructivism and finitism somewhat, though. I know they are not literally the same, but I don’t have a strong intuitive grasp of how they are related. Do you think that invalidates my question though? $\endgroup$ – user56834 Mar 4 at 7:07
  • $\begingroup$ i'm not making any claims about the validity of your question; i'm merely raising issues that are likely to make your question more difficult to understand ("unclear what you're asking"). Amongst mathematicians, the word 'countable' is rarely, if ever, used to mean 'finite', and conflating the finite and the infinite under the same term confuses things further. $\endgroup$ – Alexis Mar 4 at 7:43
  • $\begingroup$ 'Constructivism' in mathematics is the position that something doesn't 'exist', mathematically, unless we can construct an example of it. This means that proofs involving the Law of Excluded Middle (LEM) are not satisfactory: we can't argue "assume not-X; contradiction; therefore, by LEM, X", because that doesn't, in itself, give us a way to directly prove X. Finitism, howerver, is about not accepting a 'completed infinity' as a mathematical object, e.g. "the set of all natural numbers doesn't exist". One can be constructivist without being finitist, and finitist without being constructivist. $\endgroup$ – Alexis Mar 4 at 7:53
  • $\begingroup$ @Alexis, can one really be finitist without being constructivist? (the other way around I accept your point). It intuitively seems to me that any classical proof about a finite set of objects can be turned into a constructivist proof. If I'm wrong about this, then it would be nice to see a counterexample for my intuition. (also FYI, this is the first sentence of wikipedia on "countable set": "In mathematics, a countable set is a set with the same cardinality (number of elements) as some subset of the set of natural numbers. A countable set is either a finite set or a countably infinite set.") $\endgroup$ – user56834 Mar 4 at 7:59

TL;DR: Probably yes.

A formal system is a collection of axioms and inference rules over an alphabet that can also include metavariables. Any inference rule has a finite collection of premises and a single conclusion, metavariables may be replaced by arbitrary words, since all terms are also generated by the system.

There is a system modeling the notion of formal systems itself which captures all formal systems and all statements provable within them, such that every mathematical statement provable in a given context can be proven within this system.

It is quite obvious that a program generating all valid statements in this metasystem exists, yet it would run in uncountable time, even if we assume finite alphabets and words of finite length.

This program would be able to prove as much as a system allows, undecidable problems just wouldn't be included in the eventually generated result. At the end (after an uncountable amount of time), not only all provable statements of ZFC set theory, but also all such words of type theory, second-order arithmetic, ..., any system that can be specified in this very formal way will be computed.

Since you want to treat specific problems as programs, you'd just need to fit the statements returned into a certain scheme, such as the set builder notation you used. Then, the problem can be solved for $X$.

The difference between classical and constructive logic you mentioned doesn't seem fitting in my eyes though. In intitutionistic type theory (which is definitely constructive), there are types with an uncountable number of inhabitants. They need to be treated a bit more carefully, though.


Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.