Incompleteness of SOL

[Richard Kimberly Heck]

On 9/7/21 7:54 AM, Dominik Kirst wrote:
> 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.

Yes, though I would have thought that the very idea of a 'proof from
infinitely many premises' is somewhat artificial when we're working in a
conventional sort of system. So we can only say that you have such a
proof when you have one from finitely many premises. So this ends up
being a somewhat weak reason to say that the logic is incomplete: It's
incomplete in cases where you don't really have a sensible notion of
proof anyway. In particular, it leaves open the possibility that we
should have T |= A iff T |- A for all finite sets T, which would be a
pretty significant fact were it only true.


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

Which is of course equivalent to the finite sets version, given the
deduction theorem.

Riki