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