Gödel's second theorem
As a corollary to Gödel's first theorem it follows that any consistent formal system strong enough to produce arithmetic can't prove itself consistent.
Kurt Gödel (1931).
Alternative versions of Gödel’s theorem
Many versions of Gödel's proof have been advanced in the decades since his original treatment. Here are some relatively clear ones, made by writers represented on this map.
There is an algorithm that, given any consistent set of axioms, will output a polynomial equation P = 0, which in fact has no integer solutions, although this fact cannot be deduced from the given axioms.
Martin Davies, (1990, p p.659-60); also, see "Gödel’s theorem is not decisive" Box 30 on this map).
There exists an algorithm that for any recursively enumerable (r.e.) set of sentences true in the natural numbers produces a true sentence of arithmetic (a Gödel sentence) is not in that set.
Clark Glymour and Kevin Kelly (1990, p.666). Also see "Penrose can't argue for his hypothesis" in Box 28).