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?
(In)Completeness: First Order x Second Order
-
0you should maybe precise that you are talking about proof systems, not to be confused with for instance incompleteness of first-order Peano arithmetic. – 2014-07-20
1 Answers
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.
-
0@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. – 2012-11-26