For this, it is generally required that each individual proof step can be verified by a primitive recursive function or program, and hence the problem is always decidable.
Šiuo atveju paprastai reikalaujama, kad kiekvieno įrodymo pakopa būtų patikrinama pagal primityvią rekursyvinę funkciją, todėl problema yra visada išsprendžiama.