I recently came across the following claim in Eliezer Yudkowsky's post about the limits of first-order logic
“ Suppose I build a Turing machine that looks for proofs of a contradiction from first-order Peano arithmetic. If PA's consistency isn't provable in PA, then by the Completeness Theorem there must exist nonstandard models of PA where this machine halts after finding a proof of a contradiction. So first-order logic doesn't tell me that this machine runs forever - maybe it has nonstandard halting time, i.e., it runs at all standard N, but halts at -2* somewhere along a disconnected chain.”
And I’m struggling with it. To me it seems to be false - it seems like the Completeness Theorem gets you a non-standard model in which PA’s consistency is false, but not one in which it is disprovable. Therefore there claim that a Turing machine conducting a proof search would halt in this model seems to not follow? I’m quite confused by some of the wording though so perhaps I’ve misunderstood. Clarity would be much appreciated! Thanks