 The tools used in proving Gödel’s theorems also provide various important undecidability results. A theory is called decidable if the set of its theorems (sentences derivable in it) is decidable, that is (by the Church-Turing thesis) recursive. Otherwise, the theory is undecidable. Informally, being decidable means that there is a mechanical procedure which enables one to decide whether an arbitrary given sentence (of the language of the theory) is a theorem or not.