A Relation R : A → B → Ω : 𝑅 → 𝐴 𝐵 → Ω R:A\to B\to\Omega is decidable if for all x : A , y : B : 𝑥 𝐴 𝑦 : 𝐵 x:A,y:B , R ( x , y ) ∨ ¬ R ( x , y ) 𝑅 𝑥 𝑦 𝑅 𝑥 𝑦 R(x,y)\lor\lnot R(x,y) .