Editing Second-order logic (section)

==Semantics==
The semantics of second-order logic establish the meaning of each sentence. Unlike first-order logic, which has only one standard semantics, there are two different semantics that are commonly used for second-order logic: '''standard semantics''' and '''Henkin semantics'''. In each of these semantics, the interpretations of the first-order quantifiers and the logical connectives are the same as in first-order logic. Only the ranges of quantifiers over second-order variables differ in the two types of semantics.{{sfn|Väänänen|2001}}

In standard semantics, also called full semantics, the quantifiers range over ''all'' sets or functions of the appropriate sort. A model with this condition is called a full model, and these are the same as models in which the range of the second-order quantifiers is the powerset of the model's first-order part.{{sfn|Väänänen|2001}} Thus once the domain of the first-order variables is established, the meaning of the remaining quantifiers is fixed. It is these semantics that give second-order logic its expressive power, and they will be assumed for the remainder of this article.

[[Leon Henkin]] (1950) defined an alternative kind of semantics for second-order and higher-order theories, in which the meaning of the higher-order domains is partly determined by an explicit axiomatisation, drawing on [[type theory]], of the properties of the sets or functions ranged over. Henkin semantics is a kind of many-sorted first-order semantics, where there are a class of models of the axioms, instead of the semantics being fixed to just the standard model as in the standard semantics. A model in Henkin semantics will provide a set of sets or set of functions as the interpretation of higher-order domains, which may be a proper subset of all sets or functions of that sort. For his axiomatisation, Henkin proved that [[Gödel's completeness theorem]] and [[compactness theorem]], which hold for first-order logic, carry over to second-order logic with Henkin semantics. Since also the [[Skolem–Löwenheim theorem]]s hold for Henkin semantics, [[Lindström's theorem]] imports that Henkin models are just ''disguised first-order models''.<ref>*{{cite book |author=Mendelson, Elliot
 |title=Introduction to Mathematical Logic
 |edition=5th
 |series=Discrete Mathematics and Its Applications
 |type=hardcover
 |year=2009 |publisher=Chapman and Hall/CRC |location=Boca Raton
 |isbn=978-1-58488-876-5
|page=387}}
</ref>

For theories such as second-order arithmetic, the existence of non-standard interpretations of higher-order domains isn't just a deficiency of the particular axiomatisation derived from type theory that Henkin used, but a necessary consequence of [[Gödel's incompleteness theorem]]: Henkin's axioms can't be supplemented further to ensure the standard interpretation is the only possible model. Henkin semantics are commonly used in the study of [[second-order arithmetic]].

[[Jouko Väänänen]] argued that the distinction between Henkin semantics and full semantics for second-order logic is analogous to the distinction between provability in [[ZFC]] and truth in ''[[Von Neumann universe|V]]'', in that the former obeys model-theoretic properties like the Lowenheim-Skolem theorem and compactness, and the latter has categoricity phenomena.{{sfn|Väänänen|2001}} For example, "we cannot meaningfully ask whether the <math>V</math> as defined in <math>\mathrm{ZFC}</math> is the real <math>V</math> . But if we reformalize <math>\mathrm{ZFC}</math> inside <math>\mathrm{ZFC}</math>, then we can note that the reformalized <math>\mathrm{ZFC}</math> ... has countable models and hence cannot be categorical."{{Citation needed|date=December 2024}}