I think that’s right. A better example here would be the Goldbach conjecture, there we really can claim that if there is a counter-example a sufficiently persistent brute-force search will find it within a finite amount of time.
I’m not sure if this is right, but I think that means that we will never prove Goldbach to be undecidable, since doing so would prove it was true and thereby contradict the claim that it is undecidable.
I’m not sure if this is right, but I think that means that we will never prove Goldbach to be undecidable, since doing so would prove it was true and thereby contradict the claim that it is undecidable.
We could use one axiom system to prove that Goldbach is undecidable in Peano arithmetic. It would therefore be true.
I’m not sure if this is right, but I think that means that we will never prove Goldbach to be undecidable, since doing so would prove it was true and thereby contradict the claim that it is undecidable.
That seems difficult to say, though I might just be confused. I assume your intuition is along the following lines (I’m sure you’ll correct me if I’m wrong ;) ):
If Goldbach is shown to be undecidable, then this means that we can’t expect to find a counter example. Thus we can feel free to use Goldbachs conjecture, thus Goldbach’s is true. Contradiction.
The danger here seems to come from whether the intuition that “if we prove GB to be undecidable in PA, then we can safely assume that we will not ever find a counter example” is true, or if something stronger is needed to ensure the latter. I’m not sure about the truth of the claim, maybe someone can clarify?
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.
I think that’s right. A better example here would be the Goldbach conjecture, there we really can claim that if there is a counter-example a sufficiently persistent brute-force search will find it within a finite amount of time.
I’m not sure if this is right, but I think that means that we will never prove Goldbach to be undecidable, since doing so would prove it was true and thereby contradict the claim that it is undecidable.
We could use one axiom system to prove that Goldbach is undecidable in Peano arithmetic. It would therefore be true.
That seems difficult to say, though I might just be confused. I assume your intuition is along the following lines (I’m sure you’ll correct me if I’m wrong ;) ): If Goldbach is shown to be undecidable, then this means that we can’t expect to find a counter example. Thus we can feel free to use Goldbachs conjecture, thus Goldbach’s is true. Contradiction.
The danger here seems to come from whether the intuition that “if we prove GB to be undecidable in PA, then we can safely assume that we will not ever find a counter example” is true, or if something stronger is needed to ensure the latter. I’m not sure about the truth of the claim, maybe someone can clarify?
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.