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