Q:

(In)Completeness: First Order x Second Order

Why is First Order Logic complete (as proved by Gödel in his Master thesis) while Second Order Logic is not (as implied by Gödel's PhD thesis)? What are the key differences between the two systems that make them differ on such a crucial property? Is it possible to explain the differences to a working mathematician that doesn't have a formal training in mathematical logic?

A:

My intuitive understanding is that it has to do with how to interpret power types and function types. (or whatever analog is appropriate for your specific formulation of logic)
In particular, if $T$ is a type, the condition that the interpretation of the type $\mathcal{P}(T)$ must be the power set of the interpretation of the type $T$.
In other words, an interpretation of a second order (or higher) theory doesn't just have to satisfy conditions related to logic, but it must also satisfy additional set theoretic properties. The fact second order logic is incomplete, then, is the statement that one cannot express these additional set theoretic properties within the language you are trying to intrerpret.
In fact, if one suitably formalizes the meaning of power type and allows interpretations that respect the formalization without actually having to coincide with the set theoretic power sets, then second order (and higher) logic actually is complete.

