The paragraph on "Intuitionistic logic systems tend ..." is wrong to misleading at best. 1) They don't tend to be decidable unless you mean proof check is decidable in which case so do classical systems. Generally intuitionistic systems are equiconsistent with their classical counterparts and you can convert classical statements into equiprovable forms in an intuitionistic logic via something like double negation translation. 2) Type checking being decidable doesn't avoid Godel-like incompleteness. You can apply Godel's proof just fine to any intuitionistic logic (such as Heyting algebra)