General (Henkin) Structures

The standard semantics for second-order logic fixes the range of a predicate quantifier to be the full power set: $\forall X^{n}$ means for every $n$ -ary relation whatsoever. That one commitment produces both the categoricity of second-order arithmetic and the failure of compactness, completeness, and Löwenheim–Skolem. General semantics loosens exactly that commitment. It leaves the syntax of Section 4.1 untouched and changes only what the second-order quantifiers range over — from all relations to a designated collection of them. The reinterpretation makes second-order logic a disguised form of many-sorted first-order logic, and every metatheorem that first-order logic enjoys comes back with it.

Second-order logic as a many-sorted language

The route to general structures runs through the many-sorted encoding. Build a many-sorted language with $ℵ_{0}$ sorts: one individual sort, an $n$ -place predicate sort for each $n$ , and an $n$ -place function sort for each $n$ . The predicate and function parameters of the original second-order language survive, taking individual-sort arguments; equality is used only between individual terms.

Two new families of parameters connect the tiers.

Membership parameters. For each $n$ , a predicate parameter $ε_{n}$ taking one predicate-sort variable and $n$ individual terms. The atomic formula $ε_{n} X^{n} t_{1} \dots t_{n}$ says the tuple $⟨ t_{1}, \dots, t_{n} ⟩$ belongs to the relation denoted by $X^{n}$ — exactly the reading of the second-order atomic formula $X^{n} t_{1} \dots t_{n}$ .
Evaluation parameters. For each $n$ , a function parameter $E_{n}$ taking one function-sort variable and $n$ individual terms, returning an individual term. The term $E_{n} F^{n} t_{1} \dots t_{n}$ denotes the value of the function $F^{n}$ at the given arguments — exactly the reading of $F^{n} t_{1} \dots t_{n}$ .

Translating between the two languages is mechanical: attach the $ε_{n}$ and $E_{n}$ symbols to pass into the many-sorted language, strip them to return. Their only purpose is to phrase second-order application as a first-order predication, so the results of Section 4.3 apply verbatim.

Second-order application recast as first-order predication. The membership parameter turns "the tuple satisfies the relation" into an atomic formula relating a predicate-sort argument to individual-sort arguments.

Without loss of generality the membership and evaluation parameters can be taken to mean genuine membership and genuine evaluation.

The homomorphism sends a predicate-sort object $Q$ to the relation ${⟨ a_{1}, \dots, a_{n} ⟩ : ⟨ Q, a_{1}, \dots, a_{n} ⟩ \in ε_{n}^{A}}$ it induces through $ε_{n}$ , and similarly collapses each function-sort object to the operation it induces through $E_{n}$ . Because $h$ is the identity on individuals, where equality lives, the homomorphism theorem gives $⊨_{A} φ [s] \leftrightarrow ⊨_{B} φ [h \circ s]$ . Once $ε_{n}$ and $E_{n}$ are pinned to membership and evaluation they are determined by the rest of the structure, so they can be discarded entirely.

General structures

What remains after discarding $ε_{n}$ and $E_{n}$ is a structure carrying its own designated relations and functions.

An assignment $s$ now sends each predicate variable to a member of the relation universe and each function variable to a member of the function universe. Satisfaction $⊨_{A}^{G}$ is defined through the many-sorted translation, and the two clauses that matter read off the designated universes rather than the full power set:

⊨_{A}^{G} \forall X^{n} φ [s] \leftrightarrow for every R in the n -place relation universe of A, ⊨_{A}^{G} φ [s (X^{n} ∣ R)],

⊨_{A}^{G} \forall F^{n} φ [s] \leftrightarrow for every f in the n -place function universe of A, ⊨_{A}^{G} φ [s (F^{n} ∣ f)] .

Against the standard clauses, the only change is in the relation universe of $A$ in place of on $∣ A ∣$ . A quantifier that once swept the entire power set now sweeps whatever family the structure admits.

Standard versus general semantics for a predicate quantifier. On the left the quantifier ranges over the whole power set; on the right, over a chosen subfamily the general structure carries with it.

A bare pre-structure is too permissive: with an impoverished relation universe, formulas that ought to define relations would have nothing to name. The restriction that fixes this is that the designated universes be rich enough to contain everything the language can define.

Comprehension is the standing requirement that each formula-definable relation actually appears in the relation universe. A standard structure satisfies every comprehension sentence automatically, since its universe is the full power set; a general structure must certify it. The comprehension sentences, written $Γ$ , are a fixed recursive set — this is what makes the whole reduction effective.

A general structure is a two-tier object: a universe of individuals below, and admitted universes of relations and functions above, closed under definability by the comprehension axioms.

The metatheorems return

Because a general structure is, by construction, a many-sorted first-order structure satisfying the fixed axiom set $Γ$ , every first-order metatheorem transfers through the reduction of Section 4.3. A second-order sentence $σ$ is true in every general model of a set $Σ$ exactly when the many-sorted translation of $σ$ is a first-order consequence of the translation of $Σ$ together with $Γ$ . The first-order theorems for that consequence relation then apply directly.

Each is proved by adjoining $Γ$ and invoking the corresponding many-sorted theorem: for compactness, every finite subset of $Σ \cup Γ$ has a model, so the whole set does; for enumerability, general validity is many-sorted consequence of the recursive set $Γ$ , hence recursively enumerable. The enumerability theorem carries a corollary Enderton states without developing.

Completeness follows the same logic as the first-order case: the enumerability of general validity means the relation true in every general model is recursively axiomatizable, and any recursively axiomatizable consequence relation is captured by a deductive calculus. Knowing such a calculus exists, there is little reason to develop one in detail. General semantics restores the deductive completeness that the standard semantics lost.

Absolute versus general second-order logic

The standard semantics is absolute second-order logic; the designated-collection semantics is general second-order logic.

Enlarging the class of admissible structures shrinks the implications that hold. Every structure counts as a general model, so demanding truth in all of them is a stronger demand than truth in the standard models alone: if $σ$ holds in every general model of $Σ$ , then it holds in every standard model too, and $Σ ⊨ σ$ in absolute second-order logic. The converse fails. With $Σ = \emptyset$ , the general validities are a recursively enumerable set, whereas the absolute validities are not even arithmetical, so absolute validity strictly exceeds general validity.

The expressiveness–tameness trade-off. Moving right buys categoricity and definability; moving left keeps a complete calculus, compactness, and Löwenheim–Skolem.

General second-order logic sits between the two extremes: more expressive than first-order logic (it can still state comprehension and reason about relations directly) yet tame enough to keep completeness, compactness, and Löwenheim–Skolem. What it gives up in return is categoricity. Second-order induction no longer characterizes $N$ , because a general model can omit the very subset that second-order induction relies on.

Worked example (Second-order induction loses categoricity). The single sentence

σ_{ind} : \forall X (X 0 \land \forall y (X y \to X S y) \to \forall y X y)

is categorical under standard semantics yet has non-standard general models.

Under the standard reading $\forall X$ ranges over the full power set, so $σ_{ind}$ with the successor axioms forces every model to be $(N; 0, S)$ . Now read it generally. Adjoin a fresh constant $c$ and the sentences $c \neq = S^{n} 0$ , one for each numeral $S^{n} 0$ . Every finite subset is generally satisfiable, since $c$ can name a large enough standard number, so general compactness yields a general model $A$ of $A_{E}^{2}$ with an element $c^{A}$ exceeding every numeral. This $A$ still satisfies $σ_{ind}$ : the set of standard points is not in $A$ 's relation universe, so it is never a value of $X$ and cannot falsify the postulate. One sentence, categorical against the full power set, acquires non-standard models the moment the relation universe may omit a subset.

	Elementary (first-order)	General second-order	Absolute second-order
Predicate quantifier ranges over	(no such quantifier)	admitted subfamily	full power set
Compactness	holds	holds	fails
Löwenheim–Skolem	holds	holds	fails
Complete calculus	holds	holds	fails
Categorical for $N$	no	no	yes

Models of analysis

The trade-off is concrete for second-order number theory, which logicians call analysis: real numbers can be identified with sets of naturals, so quantifying over sets of naturals is quantifying over reals. Take the second-order language of arithmetic with parameters $0, S, <, +, \cdot, E$ , and let $A_{E}^{2}$ be the finitely axiomatized subtheory $A_{E}$ augmented with the second-order Peano induction postulate. Under the standard semantics every model of $A_{E}^{2}$ is isomorphic to $N$ .

General models of $A_{E}^{2}$ can depart from $N$ in two independent ways. A compactness argument, adding constants exceeding every numeral, produces nonstandard models with infinite numbers. Alternatively, a model can keep the standard individual universe but admit a non-absolute set universe smaller than the full power set of $N$ . Every countable general model is of the second kind, since the full power set is uncountable; general Löwenheim–Skolem guarantees countable models exist, and they cannot be absolute.

An $ω$ -model fixes the individuals and lets only the higher-tier universes vary, and those are governed entirely by the set universe alone.

A higher-arity relation $R$ can be compressed to a unary relation $\overset{ˉ}{R}$ by coding tuples with the recursive, and hence arithmetically definable, sequence-encoding function. Comprehension then forces the set universe to contain $\overset{ˉ}{R}$ exactly when the relation universe contains $R$ , so the one-place universe determines every other. An $ω$ -model can therefore be identified with its set universe, a subclass of the power set $P N$ , though not every subclass qualifies, only those closed enough to satisfy the comprehension sentences.

The lattice of set universes. The full power set is the one absolute model; smaller admissible classes give the other omega-models, each a comprehension-closed subclass of the power set of the naturals.

Three $ω$ -models mark the range. The full power set $P N$ is the unique absolute model. The subsets of $N$ lying in a transitive model of set theory form an $ω$ -model. The ramified analytical sets form the smallest natural $ω$ -model; they are built by transfinitely iterating the operation add every set definable over what we have so far until it closes off, which the general Löwenheim–Skolem theorem shows happens at a countable ordinal. Each admits the same standard arithmetic on individuals yet disagrees with the others on which second-order sentences hold, a disagreement that is only possible because general semantics let the set universe vary in the first place. That variation is the trade: the metatheorems of first-order logic, in exchange for the categoricity of the standard reading.¹

Enderton, §4.4. The many-sorted recasting with the $ε_{n}$ and $E_{n}$ parameters, Theorem 44A, the definitions of general pre-structure and general structure via comprehension, the general Löwenheim–Skolem, compactness, and enumerability theorems, the absolute-versus-general comparison, and the treatment of $ω$ -models of analysis including Theorem 44B are all from this section. ↩