In his first incompleteness theorem, Gödel showed us that we can
construct a sentence that denies its own provability. In his
second incompleteness theorem he showed that an example of such
a sentence is the one that asserts the inconsistency of
arithmetic. If arithmetic is consistent then it can't prove its
own consistency. On the other hand, if arithmetic is
inconsistent then we can prove anything, and hence we can prove
its consistency. Can we generalise what Gödel did? For example,
can we construct sentences that we can prove assert their own
provability? What about sentences that deny that their
provability is provable? Or what about sentences that assert
that if they're provable then it's not provable that it's
inconsistent that they imply that they're inconsistent with the
rest of arithmetic? Not only can we do these things, we can also
write a computer program that generates such theorems for us. We
can do so by working with the idea that a consistent set of
axioms describes a world, and that a set of