If there is a counter-example to Goldbach then there is an even integer which cannot be expressed as the sum of two primes. This can in principle be proven simply by listing all the ways it can be expressed as the sum of two positive integers, there are only a finite number of possibilities, and in each case showing a non-trivial factorisation of one of the numbers. All this can easily be done in PA. Thus I’m pretty confident that if Goldbach is undecidable in PA then it is true.
The difficulty, as Endoself points out, it that if we prove it is undecidable without using PA, then we can’t then teleport this statement back into PA and use it in our proof.
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 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.
%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)))) 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.
If there is a counter-example to Goldbach then there is an even integer which cannot be expressed as the sum of two primes. This can in principle be proven simply by listing all the ways it can be expressed as the sum of two positive integers, there are only a finite number of possibilities, and in each case showing a non-trivial factorisation of one of the numbers. All this can easily be done in PA. Thus I’m pretty confident that if Goldbach is undecidable in PA then it is true.
The difficulty, as Endoself points out, it that if we prove it is undecidable without using PA, then we can’t then teleport this statement back into PA and use it in our proof.
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.
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.
Huh. So essentially since
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.