This is a great explanation. There are a few things that more emphasis should have been placed on. In going over what an axiom is he should have noted that Godel's work only applies to theories which have a formal axiomatic basis and that the axioms are strong enough to encode the natural numbers enough to do certain arithmetic ops e.g. statements in the theory can be proven using induction. And maybe a bit more emphasis should have been placed on the fact that it is possible for a theory to be proven complete and consistent outside itself.

So for example, in line with the first theorem you can algorithmically verify/decide all statements in a subset of Euclidean Geometry (the subset which does not deal well with circles). And in the second part you can have theories which can verify themselves. Or that it is possible to prove a theory complete and consistent as long as you can find a suitably powerful model outside of it.