I think the philosophical profoundness of undecidability is often exaggerated. I could be way off base here, but..
Consider, in group theory, the statement “There exists an element other than the identity which squares to give the identity”. This is “undecidable” in that you can’t prove it or disprove it from the group theory axioms, and there are are groups where it’s true and groups where it’s false. However, this doesn’t make people lie awake all night worrying whether it makes maths meaningless, or whether it’s true for the “real group”.
But as soon as you get an undecidable statement about a theory of arithmetic or sets, people start worrying about whether it’s true for the “real integers” or whatever.
First, Godel’s results are much stronger than the claim that one has undecidable statements within the axiomatic system. But one also has that there’s no algorithm which can in general say whether a given statement is provable in PA (assuming that PA is in fact consistent). This is a much stronger and weirder claim.
This is also different from your group example because the natural numbers are a very concrete object. So our intuition strongly suggests that there should really be only one thing that actually looks like N in some sense. Some (although not all) senses of that are shown to be wrong by Godel’s theorems. Although what is doing more of the work here in some sense are the non-standard models of arithmetic which strictly speaking are distinct from Godel’s results.
Godel’s result about incompleteness COULD mean just that PA is inconsistent.
It would be an interesting way for the incompleteness theorem to be fulfilled. And become quite obsolete at the same time also. Except maybe as an early warning or sign that something is deeply wrong with PA.
Sure, that could be the case but that still is a much weirder situation than what Khoth is talking about. (Also, note that Godel’s theorems apply not just to PA but to the much weaker system of Robinson arithmetic so if there is an inconsistency it is probably happening at an even more fundamental level.)
I am skeptic about any infinity. I am not sure, if it is (always) paradoxical. But a theory which relates to an infinity related axiom is most likely too rich.
The concept of infinity and the concept an (infinite in any sense) god are both too ambitious for this finite world. But very persistent as we see.
Sets and Numbers are both much more central to our most basic beliefs than groups. Without an algorithmic way of determining truths about sets we may well have to adopt complete nominalism in our ontology, and interpreting modern science so as to be consistent with a nominalist ontology is no easy task.
The difference is this: Your claim about groups is independent of the axioms.
An unprovable proposition is NOT independent of the axioms. The axioms imply the truth of the statement, they just don’t allow a proof of it. That a claim is unprovable doesn’t mean it lacks a truth value.
By the way, in general, decidability is a property of languages (equivalently, of sets), not of specific sentences or claims.
In first-order logic, all valid statements are provable. The statements about natural numbers not provable from given axioms are also independent of the axioms. Both PA+Con(PA) and PA+NOT(Con(PA)) are consistent.
Does Con(PA) mean “the consequences of the peano axioms? That’s the only meaning I can think of, but then I don’t see how you could avoid inconsistency if you accept some axioms and then deny their consequences (PA + NOT (Con(PA)).
Con(PA) means the consistency of PA. It can be formalized within PA as a statement about integers, something like “there’s no integer encoding a proof in PA that 1=0”.
For an explanation of Nesov’s counterintuitive statement that PA+NOT(Con(PA)) is a consistent theory (or rather, equiconsistent with PA itself), see paragraph 48.2 in this PDF. For an explanation of how to build a model for that preposterous theory, see paragraph 2.1 in this PDF.
An unprovable proposition is NOT independent of the axioms. The axioms imply the truth of the statement, they just don’t allow a proof of it. That a claim is unprovable doesn’t mean it lacks a truth value
Is that really the case? How can the axioms imply the truth of a statement without allowing a proof of it? I thought for statements that are unprovable (and also undisprovable) there’s some model of the theory (often a pretty screwy one) where it’s true, and some model where it’s false.
There are statements that are disprovable without being provable. (Or vice-versa.) For example, a statement over the natural numbers with one universal quantifier: for all X, P(X) holds. If you find a counterexample, you’re done, but there might not be a proof. (Likewise, for finding an example of an existential claim.)
Many problems are in this category—the technical term is “semi-decidable.” For instance, the halting problem is semi-decidable. If you ever find a sequence of steps after which the machine is in a halting state, it provably halts. But there might not be any point at which you can prove that it won’t halt in the future.
Ah, I think we’re talking a bit at cross-purposes. I’m meaning proof of individual propositions in an axiomatic system, you’re meaning the algorithmic solving of a class of problems. Helpfully, the same terms can be used for both, leading to fun confusion for all.
I think the philosophical profoundness of undecidability is often exaggerated. I could be way off base here, but..
Consider, in group theory, the statement “There exists an element other than the identity which squares to give the identity”. This is “undecidable” in that you can’t prove it or disprove it from the group theory axioms, and there are are groups where it’s true and groups where it’s false. However, this doesn’t make people lie awake all night worrying whether it makes maths meaningless, or whether it’s true for the “real group”.
But as soon as you get an undecidable statement about a theory of arithmetic or sets, people start worrying about whether it’s true for the “real integers” or whatever.
What’s the difference?
There are two major differences:
First, Godel’s results are much stronger than the claim that one has undecidable statements within the axiomatic system. But one also has that there’s no algorithm which can in general say whether a given statement is provable in PA (assuming that PA is in fact consistent). This is a much stronger and weirder claim.
This is also different from your group example because the natural numbers are a very concrete object. So our intuition strongly suggests that there should really be only one thing that actually looks like N in some sense. Some (although not all) senses of that are shown to be wrong by Godel’s theorems. Although what is doing more of the work here in some sense are the non-standard models of arithmetic which strictly speaking are distinct from Godel’s results.
Couldn’t have said it better myself (vote up).
Godel’s result about incompleteness COULD mean just that PA is inconsistent.
It would be an interesting way for the incompleteness theorem to be fulfilled. And become quite obsolete at the same time also. Except maybe as an early warning or sign that something is deeply wrong with PA.
Sure, that could be the case but that still is a much weirder situation than what Khoth is talking about. (Also, note that Godel’s theorems apply not just to PA but to the much weaker system of Robinson arithmetic so if there is an inconsistency it is probably happening at an even more fundamental level.)
Robinson’s arithmetic is still an infinite one. That could be the root of all evils.
How do you feel about the infinite cyclic group?
I am skeptic about any infinity. I am not sure, if it is (always) paradoxical. But a theory which relates to an infinity related axiom is most likely too rich.
The concept of infinity and the concept an (infinite in any sense) god are both too ambitious for this finite world. But very persistent as we see.
Sets and Numbers are both much more central to our most basic beliefs than groups. Without an algorithmic way of determining truths about sets we may well have to adopt complete nominalism in our ontology, and interpreting modern science so as to be consistent with a nominalist ontology is no easy task.
The difference is this: Your claim about groups is independent of the axioms.
An unprovable proposition is NOT independent of the axioms. The axioms imply the truth of the statement, they just don’t allow a proof of it. That a claim is unprovable doesn’t mean it lacks a truth value.
By the way, in general, decidability is a property of languages (equivalently, of sets), not of specific sentences or claims.
In first-order logic, all valid statements are provable. The statements about natural numbers not provable from given axioms are also independent of the axioms. Both PA+Con(PA) and PA+NOT(Con(PA)) are consistent.
Does Con(PA) mean “the consequences of the peano axioms? That’s the only meaning I can think of, but then I don’t see how you could avoid inconsistency if you accept some axioms and then deny their consequences (PA + NOT (Con(PA)).
Con(PA) means the consistency of PA. It can be formalized within PA as a statement about integers, something like “there’s no integer encoding a proof in PA that 1=0”.
For an explanation of Nesov’s counterintuitive statement that PA+NOT(Con(PA)) is a consistent theory (or rather, equiconsistent with PA itself), see paragraph 48.2 in this PDF. For an explanation of how to build a model for that preposterous theory, see paragraph 2.1 in this PDF.
Is that really the case? How can the axioms imply the truth of a statement without allowing a proof of it? I thought for statements that are unprovable (and also undisprovable) there’s some model of the theory (often a pretty screwy one) where it’s true, and some model where it’s false.
There are statements that are disprovable without being provable. (Or vice-versa.) For example, a statement over the natural numbers with one universal quantifier: for all X, P(X) holds. If you find a counterexample, you’re done, but there might not be a proof. (Likewise, for finding an example of an existential claim.)
Many problems are in this category—the technical term is “semi-decidable.” For instance, the halting problem is semi-decidable. If you ever find a sequence of steps after which the machine is in a halting state, it provably halts. But there might not be any point at which you can prove that it won’t halt in the future.
Ah, I think we’re talking a bit at cross-purposes. I’m meaning proof of individual propositions in an axiomatic system, you’re meaning the algorithmic solving of a class of problems. Helpfully, the same terms can be used for both, leading to fun confusion for all.