Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
@Andreas, I edited the question. If you wish, you can fully narrow it down in transforming a program in a FOL + PA expression. Using Hoare logic or transforming it in a FOL + PA expression, is quite a different approach (although at the end it might not be that different). The first approach you find in the standard books and in the Wikipedia, the second not.
If the length of the proof grows slower than n itself, I think this can be fixed, by first feeding the 'n' to a fast growing function. So, we get Goodstein(f(n)). For f(n), we can take Goodstein.
domotorp, for a particular n, it is a halting problem, but the Collatz conjecture is for any n. Enumerating the proofs only works with completeness. And we know that logics are not complete.
I want to mention that in its original form, the Collatz conjecture is not a Halting problem (although someone might have found it equivalent to a Halting problem, I don't know). The Collatz conjecture is a (\Pi^0_2) question. So, even if halting problems can be expressed as chess problems on an infinite board, it doesn't mean that Collatz conjecture can be expressed as it. So, this question seems to be more complicated than 27967.
If you can prove p in PA + Con(PA) and not p in PA + not Con(PA), then p must be independent of PA (or PA is inconsistent). At that moment you can enumerate p in your solution.
Suggestion. Take also PA + not Con(PA). Then enumerate the theorems of both PA + Con(PA) and PA + non Con(PA). In the final enumeration, take the theorems that give opposite results in the two systems. Could that work?
Stefan you write "want to formalize things". The point I tried to make is that the question requires the formalization. Without it, it is not a proper question.
David, I think you answered another question from me: mathoverflow.net/questions/25430/… Give the proof, I think the answer to that question is Yes! FOL + PA extended with COR can prove Goodsteins-theorem.
Thanks for the answer (although I didn't write the question). I was searching for these proofs, but that was rather hard to find. Most proofs (such as in the Wikipedia), stop by saying that it is well-ordered.
