3 ms·

Andrej Bauer: Is it just me, or is the busy-beaver function a figment of classical mathematics? https://twitter.com/andrejbauer/status/1327670607824252928 http

by chalst 6y ago

Andrej Bauer: Is it just me, or is the busy-beaver function a figment of classical mathematics? https://twitter.com/andrejbauer/status/1327670607824252928 https://twitter.com/andrejbauer/status/1327670607824252928

qsort 6y ago
What does he mean by that? (not criticism, I genuinely don't understand).
- chriswarbo 6y ago
  There is a distinction between "constructive" mathematics (AKA "intuitionistic") and "non-constructive" mathematics (AKA "classical"). In constructive mathematics, the only way to prove that something (e.g. a number) exists is to give an algorithm that constructs it. We can do this in classical mathematics too (roughly speaking, it's a super-set of constructive mathematics); but we can also prove that something exists in another way: by disproving that it doesn't exist (i.e. a double negative). In other words, classical mathematics lets us use a proof of 'not(not(X))' as a proof of 'X'. There are some other ways to express this, which are essentially equivalent; e.g. the "law of the excluded middle" 'for all X, either X is true or not(X) is true'. These proof steps are not constructive, since knowing that not(X) is false doesn't tell us how to actually find/construct X. Likewise, the law of the excluded middle is like writing an if/then/else statement where both branches will arrive at the same result, but it doesn't tell us which of those branches to take. We usually talk about proofs being constructive or non-constructive, rather than values (e.g. numbers). A constructivist shouldn't agree with a non-constructive proof, but they should agree with an alternative, constructive proof of the same result. The interesting philosophical question being made here is: if a value's existence can only be proved non-constructively, should constructivists disbelieve in that value? In this case that value is the busy-beaver function: it can't be defined constructively, since no algorithm can decide the halting problem.
  - chalst 6y ago
    This is a good explanation. I just have one quibble: the school of constructivism that Andrej follows is not the only one; there is a Russian school that accepts Markov's principle, which is essentially the logical counterpart of the idea that there is a fact of the matter whether a deterministic Turing computation terminates. I don't know if constructivists from the Russian school allow BB to be definable, but the argument for it to be undefined is trickier on this account. https://en.wikipedia.org/wiki/Markov%27s_principle https://en.wikipedia.org/wiki/Markov%27s_principle
- zodiac 6y ago
  My guess: the definition of the BB function relies on the fact that a TM either halts or does not halt
- chalst 6y ago
  On his interpretation of constructivism, there are no mathematical constructions that are in principle non-computable. The proof that a function satisfying the property of "busy-beaverness" couldn't be computed thus is proof that the property does not determine a total function, so the classical definition is rejected as a non-constructive gesture at infinity.

by chalst 6y ago

qsort 6y ago

What does he mean by that? (not criticism, I genuinely don't understand).

chriswarbo 6y ago
There is a distinction between "constructive" mathematics (AKA "intuitionistic") and "non-constructive" mathematics (AKA "classical"). In constructive mathematics, the only way to prove that something (e.g. a number) exists is to give an algorithm that constructs it. We can do this in classical mathematics too (roughly speaking, it's a super-set of constructive mathematics); but we can also prove that something exists in another way: by disproving that it doesn't exist (i.e. a double negative). In other words, classical mathematics lets us use a proof of 'not(not(X))' as a proof of 'X'. There are some other ways to express this, which are essentially equivalent; e.g. the "law of the excluded middle" 'for all X, either X is true or not(X) is true'. These proof steps are not constructive, since knowing that not(X) is false doesn't tell us how to actually find/construct X. Likewise, the law of the excluded middle is like writing an if/then/else statement where both branches will arrive at the same result, but it doesn't tell us which of those branches to take. We usually talk about proofs being constructive or non-constructive, rather than values (e.g. numbers). A constructivist shouldn't agree with a non-constructive proof, but they should agree with an alternative, constructive proof of the same result. The interesting philosophical question being made here is: if a value's existence can only be proved non-constructively, should constructivists disbelieve in that value? In this case that value is the busy-beaver function: it can't be defined constructively, since no algorithm can decide the halting problem.
- chalst 6y ago
  This is a good explanation. I just have one quibble: the school of constructivism that Andrej follows is not the only one; there is a Russian school that accepts Markov's principle, which is essentially the logical counterpart of the idea that there is a fact of the matter whether a deterministic Turing computation terminates. I don't know if constructivists from the Russian school allow BB to be definable, but the argument for it to be undefined is trickier on this account. https://en.wikipedia.org/wiki/Markov%27s_principle https://en.wikipedia.org/wiki/Markov%27s_principle
zodiac 6y ago
My guess: the definition of the BB function relies on the fact that a TM either halts or does not halt
chalst 6y ago
On his interpretation of constructivism, there are no mathematical constructions that are in principle non-computable. The proof that a function satisfying the property of "busy-beaverness" couldn't be computed thus is proof that the property does not determine a total function, so the classical definition is rejected as a non-constructive gesture at infinity.