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)
Read more about this topic: Second-order Logic
Famous quotes containing the word results:
“Consider what you have in the smallest chosen library. A company of the wisest and wittiest men that could be picked out of all civil countries in a thousand years have set in best order the results of their learning and wisdom. The men themselves were hid and inaccessible, solitary, impatient of interruption, fenced by etiquette; but the thought which they did not uncover in their bosom friend is here written out in transparent words to us, the strangers of another age.”
—Ralph Waldo Emerson (1803–1882)