Decidable proposition

A proposition $P$ for which an algorithm exists that, in finite time, either produces a proof of $P$ or a proof of $\neg P$ - i.e., you can compute which side of $P \vee \neg P$ holds.