1. With respect to a set $S$, the property that there exists a decision procedure (an effective means) to determine whether or not any element $s$ is a member of $S$. This is to say that there exists an algorithm that can be applied to the pair $〈s,S〉$ and in a finite number of steps, will return a value of $1$ when $s\in S$ and $0$ when $s\notin S$. A related notion is that of semidecidability, in which an algorithm exists that will return $1$ when $s\in S$, but if $s\notin S$ it may return the value $0$, or may never halt. An important example of a semidecidable set is the set of formulae provable in Peano Arithmetic ($\text{PA}$). If $\text{PA}$ proves $\phi$ (i.e., if $\phi \in \text{PA}$), then due to the finitude of a proof one will in a finite number of steps come across it. However, there is no effective procedure to determine $\phi$ is not provable in $\text{PA}$.

2. With respect to a deductive system $\text{L}$, the property that either its set of theorems or its consequence relation is decidable.

3. In the context of intuitionistic logic, the property holding between a formula $\phi$ and a theory $T$ whenever $T⊢\phi \vee \neg \phi$. In the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, the decidability of a formula amounts to an effective procedure that either produces a proof of $\phi$ or produces a demonstration that $\phi$ entails an absurdity.