What does it mean to some logical statement to be provable and decidable?

Question

I am not a mathematician and trying to get deeper insight into modern logic.

It happens all the time, that statements like statement P is unprovable arise, or, more formally, $\lnot \text{Provable}(P)$. That could mean:

1. There exists no path from assumed propositions (axioms) to the $P$ that obeys rules of inference. As such, we are not able to prove $P$ and yet we might be able to prove $\lnot P$.

2. There exists no path from assumed propositions (axioms) to $P$ nor to $\lnot P$, thus we are not able to prove neither one about $P$: it is something we don't know how to reason about.

3. Both $P$ and $\lnot P$ can be proved from assumed propositions (axioms) with respect to rules of inference. That would mean that our system is not consistent and has hidden contradiction inside. That's a broken dangerous system and does not deserve our trust.

I am not that good in math to be able to illustrate all of the above mentioned options, but it feels natural to me to state unprovability in such a way.

How does modern logic answers my question? And do "provable" and "decidable" convey exactly the same meaning and are interchangeable in all contexts?

Answer 1

Provability and decidability are two distinct concepts and they are not interchangeable at all. The difference is subtle.

Saying that a statement $P$ is unprovable (in a given system) means exactly what you said in Point 1:

1. There exists no path from assumed prepositions (axioms) to $P$ that obeys rules of inference. As such, we are not able to prove $P$ and yet we might be able to prove $¬P$.

Saying that a statement $P$ is undecidable (in a given system) means exactly what you said in Point 2:

2. There exists no path from assumed prepositions (axioms) to $P$ nor to $\lnot P$, thus we are not able to prove neither one about $P$: it is something we don't know how to reason about.

However, I wouldn't say that if $P$ is undecidable then $P$ "is something we don't know how to reason about". First, saying "how to reason about it" is a bit ambiguous. Moreover, it would be better to say that the given system doesn't know how to reason about it. Indeed, in other systems $P$ can be decidable: for instance, take the system where $P$ is undecidable and add $P$ (resp. $\lnot P$) as an axiom; in the new system, $P$ is decidable and more precisely $P$ (resp. $\lnot P$) is provable.

Clearly, the fact that $P$ is provable in a system implies that $P$ is decidable in such a system (which amounts to say that undecidability of a statement implies unprovability of that statement), but the converse fails: in a system, it is possible that $\lnot P$ is provable (and hence $ P$ is decidable) but $P$ is not provable.

---

By system, I mean a set of axioms and of inference rules. Note that it is possible that in a system both $P$ and $\lnot P$ are provable (your Point 3). In that case, we say that the system is incoherent, and as a consequence (called principle of explosion) everything is provable in an incoherent system. Said differently, incoherent systems are not informative at all.

A system is said to be coherent if there is no statement $P$ such that both $P$ and $\lnot P$ are provable. In a coherent system, the situation you described in Point 3 is impossible. In a coherent system it is possible (but not necessary) to have unprovable and/or undecidable statements.

---

Concerning decidability, what I mentioned above is the meaning of "decidable" when referred to a statement. Unfortunately, in logic there is another meaning of "decidable", but referred to a system, not a statement. A system is decidable if there is an effective method (an algorithm) for determining whether arbitrary statements are provable or not is that system.