# Is the first-order incompleteness of a theory (like arithmetics, set theory or logic itself) avoidable in a second or higher-order axiomatizations?

Can we avoid the first-order incompleteness of a theory (like arithmetics or set theory) in a second-order theory which contains the previous? How does it depend on the chosen semantics or models? If we can't, can we, at least, construct a second or higher-order theory which contains the previous and avoids the undecidability of its first-order propositions? Can we do it in general?, i.e., if we have a n-order theory with undecidable propositions, can we construct a n+k-order theory which contains the last and avoids (that is, in where these are decidable) its n or lower-order undecidable propositions? How does it depend on the chosen semantics or models?

What if we change the theory by the logic itself? If we have a n-order logic (with n>1 to ensure the incompleteness under some semantics) with undecidable propositions, can we construct a n+k-order logic which contains the previous and avoids (that is, in where these are decidable) its n or lower-order undecidable propositions? How does it depend on the chosen semantics or models?

Can we construct a second or higher-order complete arithmetics? How does it depend on the chosen semantics or models?

• The second incompleteness theorem applies to any sufficiently strong theory that is consistent and includes enough arithmetic. It makes no difference whether the theory is first-order, second-order, or even in some other kind of logic that is not "$n$-th order" at all. The only restriction is that the theory and deductive system have to be effective. – Carl Mummert Nov 4 '14 at 2:17
• I wonder, though, whether this has already been asked on this site. – Carl Mummert Nov 4 '14 at 2:20
• I'm not sure if this is an aside, but you can construct a first-order complete axiomatization of arithmetic: the trick is that the axiomatization won't be Turing decidable. – Hurkyl Nov 4 '14 at 4:33

Let Goedel speak to you in his own words: "As will be shown in Part II of this paper, the true reason for the incompleteness inherent in all formal systems of mathematics is that the formation of ever higher types can be continued into the transfinite (see Hilbert 1925, p. 184 [in van Heijenoort, p.387--my comment]), while in any formal system at most denumerably many of them are available. For it can be shown that the undecidable propositions constructed here become decidable whenever appropriate higher types are added (for example, the type $\omega$ to the system P). An analogous situation prevails for the axiom system of set theory." This is footnote 48a of his paper "On formally undecidable propositions of Principia mathematica and related systems I" and is found on pg 610 of van Heijenoort's book, "From Frege to Goedel". The system P mentioned in the footnote is "essentially the system obtained when the logic of PM [Principia mathematica--my comment] is superposed upon the Peano axioms" (Goedel, "On formally undecidable propositions...." found in van Heijenoort, p. 599). I hope this helps.