Gödel not just good for incompleteness

This theorem is not provable

Kurt Gödel was famous for his incompleteness theorems (GIT) which entirely destroyed Hilbert's program (not really, just changed it's direction) and changed the face of philosophy of mathematics (probably should have but frankly not really), created recursive function theory and proof theory (pretty much).

But he is also well known within logic for many ground-breaking results there.

These results are

• proved the completeness theorem of predicate calculus (his PhD thesis, just before his incompleteness theorems, causing thousands of people-years in confusion because they refer to two different definitions of 'completeness, syntactic (for his PhD) and semantic (for GIT)
• created provability logic within modal logic (namely that  Intuitionistic Propositional Logic is Interpretable in S4 ) 
• proved the consistency of the continuum hypothesis and the axiom of choice with set theory (just one half of independence of these two axioms from ZF set theory, Paul Cohen did the negative side).

I suppose there are other things that he did that would have made him famous if it weren't for each one of the above.