. Namely, one can show that the undecidable sentences which have been constructed here always become decidable through adjunction of sufficiently high types (e.g. of the type ω to the system **P** ). A similar result holds for the axiom systems of set theory