Timeline for Finite verification for theorems due to Busy Beaver numbers
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Jul 16 at 5:05 | vote | accept | Ivan Galakhov | ||
| S Jul 16 at 5:04 | vote | accept | Ivan Galakhov | ||
| S Jul 16 at 5:05 | |||||
| Jul 16 at 5:04 | vote | accept | Ivan Galakhov | ||
| S Jul 16 at 5:04 | |||||
| Jul 15 at 16:19 | comment | added | usul | Yes, it turns out the statement is trivial, but the "nontrivial intuition" the question is trying to capture is interesting, and addressed nicely in Sam Hopkins' comment. Namely, if we had an oracle for BB(n), we could automate the proof/disproof of any well-defined claim. | |
| Jul 14 at 23:45 | answer | added | C7X | timeline score: 18 | |
| Jul 14 at 22:41 | comment | added | Leif Sabellek | I think the statement in the opening post is trivially true: If Goldbach's Conjecture ist true, any N works. If the Conjecture is false, then take N as the smallest counter example. | |
| Jul 14 at 0:39 | history | became hot network question | |||
| Jul 13 at 21:54 | comment | added | Zuhair Al-Johar | Continuation... This way we assure matters be confined to standard naturals. Then ask if $\sf PA$ can prove an inference rule $I_n$ for some metatheoretic $n$, where $I_n$ is the rule: $$ {\sf GC}_n \\ \overline{\forall x \in N: {\sf GC}(x)}$$ Where ${\sf GC}(x)$ is the usual statement of Goldbach's conjecture (here $x$ range over all naturals standard and non-standard). | |
| Jul 13 at 21:54 | comment | added | Zuhair Al-Johar | I think it is better to ask for a constructive proof of your statement, since non-constructive proofs trivialize matters. Also, I think one can even present matters in classical $\sf PA$, we describe $\sf GC_n$ up to metatheoretic $n$ to mean every even number up to $\sf SSS....S_n(0)$ that is greater than $4$ is the sum of two even numbers. | |
| Jul 13 at 18:38 | answer | added | Joel David Hamkins | timeline score: 51 | |
| Jul 13 at 16:50 | answer | added | Will Sawin | timeline score: 31 | |
| Jul 13 at 16:44 | comment | added | Sam Hopkins | Here's maybe a different way to think about things, that shows this isn't really about Turing machines or Goldbach's conjecture or whatever. Suppose we have some logical formalism where mathematical statements and their proofs can be represented by finite strings. For each $n$, there must be some $N$, so that all statements of length $n$ have either a proof of length $N$ or a disproof of length $N$, or are independent of our formal system. If we knew what this $N$ was in terms of $n$ we could simply check all proofs/disproofs of our statement, which is a "finite" and "automatic" thing to do. | |
| Jul 13 at 16:39 | history | edited | Ivan Galakhov | CC BY-SA 4.0 |
added 2 characters in body
|
| S Jul 13 at 16:38 | review | First questions | |||
| Jul 13 at 16:57 | |||||
| S Jul 13 at 16:38 | history | asked | Ivan Galakhov | CC BY-SA 4.0 |