Timeline for Finding the largest integer describable with a string of symbols of predefined length
Current License: CC BY-SA 2.5
2 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 26, 2010 at 20:07 | comment | added | Joel David Hamkins | As you suspected, you do need $\omega$-consistency here; mere consistency is insufficient, since if the theory has no $\omega$-model, then it could be that the theory proves the program halts only in nonstandard time. For example, the program that searches for a proof of a contradiction in PA is provably halting in $PA+\neg\text{Con}(PA)$, but it doesn't actually halt. But if the theory is $\omega$-consistent, then when it proves that a program halts, it really does halt. | |
| Jul 22, 2010 at 4:21 | history | answered | Richard Borcherds | CC BY-SA 2.5 |