# (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?

-
The title is now out of sync with the body of the question. Antd anyway, don't you really mean why is first-order logic complete and second-order logic incomplete? – Peter Smith Nov 26 '12 at 8:24
You're right, @Peter, "First Order x Second Order" expresses my doubts more appropriately. – Ari Nov 27 '12 at 21:56
The title is now incomprehensible. – Chris Eagle Nov 27 '12 at 22:06
you should maybe precise that you are talking about proof systems, not to be confused with for instance incompleteness of first-order Peano arithmetic. – Denis Jul 20 '14 at 23:47

## 1 Answer

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.

-
!Hurkyl: the fact you allude to in your final paragraph is indeed well known; it was shown by Leon Henkin in 1950. – Carl Mummert Nov 26 '12 at 3:00
@Carl: Thanks a lot! I was pretty sure that had to be the case, but somehow I don't recall ever managing to encounter an explicit statement of the fact. – Hurkyl Nov 26 '12 at 3:38