Huh. So basically since (if you’ll excuse some sort of sloppy notation as well as sloppy formatting, I just can’t seem to get the latex to fit together nicely on this)
%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
%20(PA%20\nvdash%20\forall%20(prime:y,z%20%3C%20x)%20(x%20\neq%20y+z))]%0A)
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.
this generalizes to every proposition that has effectively computable counterexamples
I think so, it certainly generalises to any problem where counter-examples can always be proven in PA, I don’t know enough about the subject to know whether this is equivalent to computability.
Huh. So basically since (if you’ll excuse some sort of sloppy notation as well as sloppy formatting, I just can’t seem to get the latex to fit together nicely on this)
and
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.
I think so, it certainly generalises to any problem where counter-examples can always be proven in PA, I don’t know enough about the subject to know whether this is equivalent to computability.