Incompleteness of SOL

[Tennant, Neil]

Dear Dominik,
The answers to your questions are positive.
Please see my book Natural Logic, Edinburgh University Press, 1978.
Best regards,
Neil Tennant

Get Outlook for iOS<https://aka.ms/o0ukef>
________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of Richard Kimberly Heck <richard_heck at brown.edu>
Sent: Tuesday, September 7, 2021 6:28:35 PM
To: Dominik Kirst <kirst at cs.uni-saarland.de>; fom at cs.nyu.edu <fom at cs.nyu.edu>
Subject: Re: Incompleteness of SOL

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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210908/57561683/attachment-0001.html>