Incompleteness of SOL

[Dominik Kirst]

Dear FOM-members,

I have a question regarding the incompleteness of second-order logic: in textbooks (e.g. Shapiro 1991) the incompleteness of sound and effective deduction systems for SOL is usually obtained as a consequence of Gödel’s incompleteness theorem. However, it is usually also shown that, for instance due to the categoricity of second-order PA, the standard semantics for SOL fails to be compact. Therefore trivially no sound deduction system (compact by the convention that T |- A if T’ |- A for some finite T’ <= T) can be complete, at least in the strong sense that T |= A would imply T |- A for all A and possibly infinite T.

Has this argument been explicitly mentioned in the literature and compared to the more heavy-weight argument invoking Gödel’s incompleteness? And is the reason for the latter being the standard proof that it also refutes the weaker form of completeness where |= A implies |- A for all A?

Thanks for your help,
Dominik


-----------------------------------------
Programming Systems Lab
Saarland University
http://www.ps.uni-saarland.de/~kirst/