3 ms·
No, since a proof is finite. When you enumerate Turing machines to generate a proof you execute the first n machines for n steps. At some point some machine mus
by rrobukef 7y ago
No, since a proof is finite. When you enumerate Turing machines to generate a proof you execute the first n machines for n steps. At some point some machine must decide something, so some n is the bound.
- memling 7y ago> No, since a proof is finite. When you enumerate Turing machines to generate a proof you execute the first n machines for n steps. At some point some machine must decide something, so some n is the bound. Thanks. It's been awhile for me, so if you could bear with the perhaps simple question: do we avoid undecidability here by the finitude of the proof or by only running a finite number of steps? It seems to me like there are three states for any solver: (1) it responds in the negative (this is not a proof), (2) it responds in the positive (this is a proof, you're done), or (3) I'm still trying figure it out. Do we fold the 3d case into the 1st by saying that we'll only iterate n steps before terminating? Or am I missing the point entirely?