Timeline for Finite verification for theorems due to Busy Beaver numbers
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 21 at 13:12 | comment | added | KConrad | Here is the paper mentioned in my previous comment: D.R. Heath-Brown, Prime Twins and Siegel Zeros, Proc. London Math. Soc. 47 (1983), 193-224. On the 4th page (in the introduction) he wrote: "One must be careful in interpreting such ineffective results, as the following proposition shows: there exists a constant $C$ with the property that to prove the number of prime twins to be infinite, it suffices to find a pair $p, p+2$ with $p > C$. (Define $C=1$ if there are infinitely many such twins, and otherwise set $C=\max\{p: p,p+2 {\sf \ both \ prime}\}$.)" His $C$ was really denoted $C^{(3)}$. | |
| Jul 15 at 13:05 | comment | added | Joel David Hamkins | The Berkeley party with Lenstra would have occurred in the late 80s. But I would guess that this observation was known even well before that time. | |
| Jul 15 at 12:49 | comment | added | KConrad | I heard exactly the same joke theorem about twin primes during a colloquium talk by Iwaniec at Ohio State in the late 1990s. Later I happened to see it in the introduction to some published paper (I think it was in Inventiones) as a warning about ineffective constants in certain kinds of results, but I no longer recall the exact paper. Maybe someone reading this does know that paper and could add it here as a comment. | |
| Jul 14 at 21:41 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
Improved exposition again.
|
| Jul 14 at 17:03 | comment | added | LegionMammal978 | True, I suppose it depends on your reference point for "many": I'd consider a dozen to be plenty enough, given how quickly the function grows. I remain optimistic about provability for "small" machines in principle, since the known-"hard" machines are all just gnarly statements in number theory, which we usually presume not to be too powerful in proof-theoretic terms. (Still, there are constructive systems which can prove infinitely many $\operatorname{BB}$ values: it's just that they're all either uncomputable or inconsistent!) | |
| Jul 14 at 16:27 | comment | added | Joel David Hamkins | There are not so many pairs for which one can prove constructively that $\text{BB}(n)=N$, since these become all independent of ZFC even in classical logic for relatively small values of $n$. One cannot even prove upper bounds on the values in ZFC, from some small value of $n$ onward. (The exact place this occurs is open and is itself in any case independent of ZFC.) | |
| Jul 14 at 16:20 | comment | added | LegionMammal978 | @GeoffreyIrving To make what Z. A. K. says more explicit, when we say that $\operatorname{BB}(n)\leq N$, we say that "for all $n$-state 2-symbol machines $M$, either $M$ halts in $\leq N$ steps, or $M$ doesn't halt at any step". Depending on the system, there are many particular pairs $(n,N)$ for which constructive logic can prove $\operatorname{BB}(n)\leq N$. But (assuming consistency) constructive logic cannot prove that "for all $n$, there exists an $N$ such that $\operatorname{BB}(n)\leq N$", since this requires LEM. | |
| Jul 14 at 15:08 | comment | added | Z. A. K. | @GeoffreyIrving: You can easily define "*$x$ is the $n$th Busy Beaver number*" in all constructive foundational systems (HA, MLTT, CZF) in widespread use, and then use this definition to pin down small values of $BB$, for example that 6 is the 2nd Busy Beaver number. You can't normally construct $BB : \mathbb{N} \rightarrow \mathbb{N}$ as a bona fide total function, since these system usually only construct computable $\mathbb{N} \rightarrow \mathbb{N}$ functions, which $BB$ isn't. | |
| Jul 14 at 11:19 | comment | added | Will Sawin | @GeoffreyIrving I'm almost certain that the answer is no. | |
| Jul 14 at 8:46 | comment | added | Geoffrey Irving | Is constructive logic able to even define the BB function? | |
| Jul 14 at 3:11 | comment | added | Z. A. K. | @IvanGalakhov: There need not be a constructive proof of $\exists N. (\forall x < N. P(x)) \rightarrow \forall x. P(x)$ even if $P(-)$ is very simple, e.g. computable. In fact a sufficiently constructive theory (e.g w/ numerical existence property) can't prove this for a computable predicate $P$ unless it also proves one of $\forall x. P(x)$ or $\neg \forall x. P(x)$. The way to think about it is not so much "it's enough to check if Goldbach holds up to $BB(n)$ for some $n$" and much closer to "we'd have to first settle Goldbach to pin down the value of $BB(n)$ for large enough $n$". | |
| Jul 14 at 0:59 | comment | added | Ivan Galakhov | That was my intention, yes. I see now that this results is fairly boring with LEM, so I guess a better question would be if this kind of statement is constructible. | |
| Jul 13 at 22:28 | comment | added | Zuhair Al-Johar | @JoelDavidHamkins, look at the details of his question. He says "construct" a Turing machine that can check ... this seems to restrict working with standard naturals. See, my comment on the original posting. There is a constructive touch in his preamble. It certainly feels that the exposition as a formula in the way he did, actually doesn't capture the original intention. He is speaking about an inference rule with standard naturals. And specifically about constructing such a rule. Anyhow, I might have exaugurated his wording? | |
| Jul 13 at 21:56 | comment | added | Joel David Hamkins | @ZuhairAl-Johar I disagree. The question has nothing to do with intuitionistic logic, which definitely does not settle any nontrivial values of the BB function in any case---they are all independent of ZFC even, and there is no hope of constructive proofs of these things without settling the underlying question constructively as Will describes. The question and answers rather are about this certain trivial form of argument, a special proof by cases that is sometimes confusing for beginners, but which is also entirely a classical logic phenomenon. | |
| Jul 13 at 21:08 | comment | added | Zuhair Al-Johar | @WillSawin, I see, so the OP question would be non-trivial if he asked for a constructive proof of his statement regarding Goldbach's conjecture, or even for a similar statement regarding the twin prime conjecture. I mean for these particular cases the question is non-trivial I suppose. And in reality I think this is the original intention behind such questions, since LEM trivialize matters for these cases. | |
| Jul 13 at 20:13 | comment | added | Will Sawin | @ZuhairAl-Johar Since the proof uses LEM, it is certainly not constructively valid, and the relevant question is "can this be modified to be constructively valid?" The answer is "no" if you interpret the question as, "For an arbitrary predicate $P$, does there exist a constructive proof of $\exists x ( P(x) \implies \forall y P(y))$?". The statement for the twin primes conjecture or Goldbach conjecture might of course admit a completely different constructive proof, e.g. if these conjectures themselves admit constructive proofs. | |
| Jul 13 at 19:57 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
Improved exposition
|
| Jul 13 at 19:15 | comment | added | Zuhair Al-Johar | @WillSawin, Joel David Hamkins, Is this a constructive proof? I mean is it valid in constructive or intuitionistic logic? | |
| Jul 13 at 19:07 | comment | added | Joel David Hamkins | See also the drinker's paradox: en.wikipedia.org/wiki/Drinker_paradox. In any nonempty bar, there is a person, such that if that person is drinking at that moment, then everyone is drinking at that moment. | |
| Jul 13 at 19:04 | comment | added | Will Sawin | I heard this argument from a graduate student of Peter Sarnak, who said that he stated the theorem "There exists an (ineffective) $\sigma>1/2$ such that if the Riemann zeta function has no zeroes with real part $>\sigma$ then the Riemann hypothesis is true" as an example of the weakness of results with ineffective constants. I don't know if this kind of idea is particularly common among number theorists. | |
| Jul 13 at 18:51 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 66 characters in body
|
| Jul 13 at 18:44 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 171 characters in body
|
| Jul 13 at 18:38 | history | answered | Joel David Hamkins | CC BY-SA 4.0 |