Second-order Logic - Metalogical Results

Metalogical Results

It is a corollary of Gödel's incompleteness theorem that there is no deductive system (that is, no notion of provability) for second-order formulas that simultaneously satisfies these three desired attributes:

• (Soundness) Every provable second-order sentence is universally valid, i.e., true in all domains under standard semantics.
• (Completeness) Every universally valid second-order formula, under standard semantics, is provable.
• (Effectiveness) There is a proof-checking algorithm that can correctly decide whether a given sequence of symbols is a valid proof or not.

This corollary is sometimes expressed by saying that second-order logic does not admit a complete proof theory. In this respect second-order logic with standard semantics differs from first-order logic; Quine (1970, pp. 90–91) pointed to the lack of a complete proof system as a reason for thinking of second-order logic as not logic, properly speaking.

As mentioned above, Henkin proved that the standard deductive system for first-order logic is sound, complete, and effective for second-order logic with Henkin semantics, and the deductive system with comprehension and choice principles is sound, complete, and effective for Henkin semantics using only models that satisfy these principles.

The compactness theorem and the Löwenheim-Skolem theorem do not hold for full models of second-order logic. They do hold however for Henkin models. (Väänänen 2001)