A statement can only be said to be provable or unprovable within some axiom system. Gödel’s first incompleteness theorem says that for any strong enough axiom system talking about the integers, there will exist true statements about the integers that the system cannot prove.
(ETA ignore the following, it’s wrong. Wow I’m really embarrassed right now. Whoever is reading this, please do me a favor and downvote my comment to oblivion—I don’t want to delete it because it has replies.)
If you proved the Collatz conjecture to be “undecidable either way” in some reasonable axiom system (as opposed to just unprovable in that system), that would imply the conjecture is true about the “actual integers”, because having no counterexamples is the same as being true.
Does undecidability really mean truth for the Collatz conjecture? Suppose it’s undecidable because in the “actual integers” there’s a starting value where the sequence grows indefinitely but there’s no way to prove that. Is that a possible situation?
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.
What about Godel’s first and second incompleteness theorems? They were not proven using any axiom system. Godel’s proof worked by substituting certain characters in PM with abbreviations, and then abbreviating those abbreviations, etc. He did so in a way that created a string of PM which stated that “this string’s Godel number is not a PM number.” He then used reasoning as old as the famous Cretan to show that that statement could never be consistently decided upon.
These results were shown about axiomatic systems of sufficient strength, but not inside of anyone system. Godel’s completeness theorem of first order logic functions in a similar way (reasoning about a formal system rather than within it). All of these results are achieved by model theoretic methods; if you want to know how you prove something outside of a proof theory look at model theory.
Gödel’s theorems can be formalized. Here’s a formal proof of the first one in Coq. Also, paragraph 8.4 there explains how the second incompleteness theorem can be proved by formalizing the proof of the first one within the system in question.
Model theory is not “platonic”, it lives within an ambient set theory. There are different axiomatizations of set theory, e.g. ZFC, which give rise to different “model theories”. An example from Wikipedia:
There is a finite second-order theory whose only model is the real numbers if the continuum hypothesis holds and which has no model if the continuum hypothesis does not hold. This theory consists of a finite theory characterizing the real numbers as a complete Archimedean ordered field plus an axiom saying that the domain is of the first uncountable cardinality.
I know that you can formalize Godel’s incompleteness theorems, but they were not formalized originally, nor did they need to be formalized to be valid deductive arguments.
Now, you can’t really formalize Godel’s proof without abbreviation, this I know. The godel number of sentence G is a huge number that none of us could ever write down and that a computer would probably have a hard time holding as a value. Have you ever seen a proof of Euclid’s prime theorem in PA? Euclid gave a 6 step proof, in PA there are over 50 steps because every single peice of reasoning gets written down. To actually directly reference every peice of reasoning in godel’s proof is something Godel never does in undecidable props of PM and something that he has no need to do.
To be a valid deductive argument, a theorem must be formalizable. That doesn’t depend on accidental facts like whether its original presentation was formalized or not.
A statement can be proven outside of a formal system (I should have said from the beginning: “outside of a complete and consistent formal system) . There is no complete and consistent axiomatization of the differential calculus as shown by Godel’s first and second theorem, yet I think we can all agree that there are proofs in the calculus.
Your comment seems confused to me. There’s also no complete and consistent axiomatization of the integers, but the incomplete axiomatizations that we know allow us to formally prove statements like 2+2=4. Same for calculus.
The calculus was created before the innovation of formal systems in the 20th century. Mathematical reasoning might be capable of being represented by a formal system, but it is not identical with a formal system. If by “axiom system” you mean formal system, then in a very precise way there is no axiom system for the calculus and one has never been used. Any formal system that accurately modeled the calculus (regardless of its completeness or consistency) would be so much more austere and cluttered than the calculus itself, that it would be of no practical use.
The proofs in the calculus are not proofs in a completely syntactic system, the axioms and theorems require some degree of interpretation. Likewise, we don’t actually use PA to prove most statements about the natural numbers, we use the basic agreements we all have about what numbers act like and about what happens when you combine them by certain operators.
The calculus was created before the innovation of formal systems in the 20th century.
So was arithmetic. That is irrelevant to the possibility of formalising them.
Mathematical reasoning might be capable of being represented by a formal system, but it is not identical with a formal system. If by “axiom system” you mean formal system, then in a very precise way there is no axiom system for the calculus and one has never been used.
Can you elucidate this precise sense? Calculus is just as formalisable as every other branch of mathematics.
The proofs in the calculus are not proofs in a completely syntactic system, the axioms and theorems require some degree of interpretation.
What do you mean? I can prove d(x^2)/dx = 2x in as exhaustively complete detail as you want. So can these people and they probably have the proof online somewhere (the web site makes it very difficult to actually read their repository of formalised mathematics). Here’s a road map, starting from Peano arithmetic.
Construct the negative integers as equivalence classes of pairs of Peano integers: (a,b) and (c,d) are equivalent if a+d=b+c.
Do a similar extension to get the rational numbers.
I am not arguing about the possibility of formalizing the calculus, I am talking about the necessity. There have been proofs without formal systems and there will continue to be. All of these proofs might be formalize-able, but they were proofs before they were shown to be such.
What I meant by “there is a very formal sense in which the calculus cannot be formalized.” is that you can’t have a complete and consistent axiomatization of the reals. I apologize for the ambiguity. But unlike finitism, frst order logic, boolean arithmetic, category theory, and I’m sure many more, calculus and arithmetic cannot be completely and consistently axiomatized.
I am not arguing about the possibility of formalizing the calculus, I am talking about the necessity. There have been proofs without formal systems and there will continue to be. All of these proofs might be formalize-able, but they were proofs before they were shown to be such.
People built buildings before mechanics and materials science, but at some point in the development of the technology, you need those to get any further. It’s the same with mathematics. The formal apparatus isn’t what people do mathematics in, but it’s a necessary foundation. Without it you get informal arguments that no-one is quite sure are really valid, as was the case for calculus before the epsilon-delta definition of a limit was worked out. (It was more than a century later before someone was able to make rigorous the original talk of infinitesimals.)
You can proof something outside of a formal system. Algebra and the differential calculus are not formal systems, but you may have proofs within them. Look up model theory.
A statement can only be said to be provable or unprovable within some axiom system. Gödel’s first incompleteness theorem says that for any strong enough axiom system talking about the integers, there will exist true statements about the integers that the system cannot prove.
(ETA ignore the following, it’s wrong. Wow I’m really embarrassed right now. Whoever is reading this, please do me a favor and downvote my comment to oblivion—I don’t want to delete it because it has replies.)
If you proved the Collatz conjecture to be “undecidable either way” in some reasonable axiom system (as opposed to just unprovable in that system), that would imply the conjecture is true about the “actual integers”, because having no counterexamples is the same as being true.
Does undecidability really mean truth for the Collatz conjecture? Suppose it’s undecidable because in the “actual integers” there’s a starting value where the sequence grows indefinitely but there’s no way to prove that. Is that a possible situation?
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.
Argh! Sorry, in a hurry I got Collatz mixed up with something else, so the second half of my comment was completely stupid.
Only if you can’t proof that given that starting value the function will always rise, but that is an unlikely situation.
What about Godel’s first and second incompleteness theorems? They were not proven using any axiom system. Godel’s proof worked by substituting certain characters in PM with abbreviations, and then abbreviating those abbreviations, etc. He did so in a way that created a string of PM which stated that “this string’s Godel number is not a PM number.” He then used reasoning as old as the famous Cretan to show that that statement could never be consistently decided upon.
These results were shown about axiomatic systems of sufficient strength, but not inside of anyone system. Godel’s completeness theorem of first order logic functions in a similar way (reasoning about a formal system rather than within it). All of these results are achieved by model theoretic methods; if you want to know how you prove something outside of a proof theory look at model theory.
Gödel’s theorems can be formalized. Here’s a formal proof of the first one in Coq. Also, paragraph 8.4 there explains how the second incompleteness theorem can be proved by formalizing the proof of the first one within the system in question.
Model theory is not “platonic”, it lives within an ambient set theory. There are different axiomatizations of set theory, e.g. ZFC, which give rise to different “model theories”. An example from Wikipedia:
I know that you can formalize Godel’s incompleteness theorems, but they were not formalized originally, nor did they need to be formalized to be valid deductive arguments.
Now, you can’t really formalize Godel’s proof without abbreviation, this I know. The godel number of sentence G is a huge number that none of us could ever write down and that a computer would probably have a hard time holding as a value. Have you ever seen a proof of Euclid’s prime theorem in PA? Euclid gave a 6 step proof, in PA there are over 50 steps because every single peice of reasoning gets written down. To actually directly reference every peice of reasoning in godel’s proof is something Godel never does in undecidable props of PM and something that he has no need to do.
To be a valid deductive argument, a theorem must be formalizable. That doesn’t depend on accidental facts like whether its original presentation was formalized or not.
A statement can be proven outside of a formal system (I should have said from the beginning: “outside of a complete and consistent formal system) . There is no complete and consistent axiomatization of the differential calculus as shown by Godel’s first and second theorem, yet I think we can all agree that there are proofs in the calculus.
Your comment seems confused to me. There’s also no complete and consistent axiomatization of the integers, but the incomplete axiomatizations that we know allow us to formally prove statements like 2+2=4. Same for calculus.
The calculus was created before the innovation of formal systems in the 20th century. Mathematical reasoning might be capable of being represented by a formal system, but it is not identical with a formal system. If by “axiom system” you mean formal system, then in a very precise way there is no axiom system for the calculus and one has never been used. Any formal system that accurately modeled the calculus (regardless of its completeness or consistency) would be so much more austere and cluttered than the calculus itself, that it would be of no practical use.
The proofs in the calculus are not proofs in a completely syntactic system, the axioms and theorems require some degree of interpretation. Likewise, we don’t actually use PA to prove most statements about the natural numbers, we use the basic agreements we all have about what numbers act like and about what happens when you combine them by certain operators.
So was arithmetic. That is irrelevant to the possibility of formalising them.
Can you elucidate this precise sense? Calculus is just as formalisable as every other branch of mathematics.
What do you mean? I can prove d(x^2)/dx = 2x in as exhaustively complete detail as you want. So can these people and they probably have the proof online somewhere (the web site makes it very difficult to actually read their repository of formalised mathematics). Here’s a road map, starting from Peano arithmetic.
Construct the negative integers as equivalence classes of pairs of Peano integers: (a,b) and (c,d) are equivalent if a+d=b+c.
Do a similar extension to get the rational numbers.
Use Dedekind cuts to define real numbers.
Use epsilon-delta definitions to define limits.
With limits, define derivatives.
Calculate d(x^2)/dx: ((x+delta)^2 - x^2)/delta = 2x + x*delta --> 2x as delta --> 0. QED.
I am not arguing about the possibility of formalizing the calculus, I am talking about the necessity. There have been proofs without formal systems and there will continue to be. All of these proofs might be formalize-able, but they were proofs before they were shown to be such.
What I meant by “there is a very formal sense in which the calculus cannot be formalized.” is that you can’t have a complete and consistent axiomatization of the reals. I apologize for the ambiguity. But unlike finitism, frst order logic, boolean arithmetic, category theory, and I’m sure many more, calculus and arithmetic cannot be completely and consistently axiomatized.
People built buildings before mechanics and materials science, but at some point in the development of the technology, you need those to get any further. It’s the same with mathematics. The formal apparatus isn’t what people do mathematics in, but it’s a necessary foundation. Without it you get informal arguments that no-one is quite sure are really valid, as was the case for calculus before the epsilon-delta definition of a limit was worked out. (It was more than a century later before someone was able to make rigorous the original talk of infinitesimals.)
You can proof something outside of a formal system. Algebra and the differential calculus are not formal systems, but you may have proofs within them. Look up model theory.