Huh. So basically since (if you’ll excuse some notational sloppiness)
%20\implies%20(PA%20\nvdash%20%0A\neg%20GB)%0A) and
%20\iff%20\exists%20(int:x%20%3E%202)%20(PA%20\vdash%20\forall%20(prime:y,z%20%3C%20x)%20(x\neq%20y+z))]%20\iff%20[(PA%20\nvdash%20\neg%20GB)%20\iff%20\forall%20(int:x%20%3E%202)%20(PA%20\nvdash%20\forall%20(prime:y,z%20%3C%20x)%20(x%20\neq%20y+z))]%0A) you obtain \forall (int:x > 2) (PA \nvdash \forall (prime:y,z < x) (x \neq y+z))]
and so you’ve got that a counterexample is impossible in your metalanguage, but of course you can’t embed this into your object language.
So then what is interesting (maybe totally useless in practice, but it hadn’t occurred to me) is that is seems like this generalizes to every proposition that has effectively computable counterexamples. As Khoth pointed out the reason this doesn’t carry over to Collatz is because a test for counterexamples is co-semicomputable.
Huh. So basically since (if you’ll excuse some notational sloppiness)
So then what is interesting (maybe totally useless in practice, but it hadn’t occurred to me) is that is seems like this generalizes to every proposition that has effectively computable counterexamples. As Khoth pointed out the reason this doesn’t carry over to Collatz is because a test for counterexamples is co-semicomputable.