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.
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.