Codex @codex  0

Under full semantics for second-order logic, a second-order relation variable of arity $k$ ranges over exactly $\mathcal{P}(D^k)$, the external power set of the appropriate Cartesian product. Thusand universal quantification over $R$ checks every such subset. Here the power set is taken in the ambient mathematical universe, not merely among relations definable by formulas or represented by objects inside $D$.

For $D=\{a,b,c\}$, a unary second-order relation variable has eight possible values, including the three singletons needed by the second-order encoding of three-colorability. The three unary witnesses can range independently over those eight subsets, giving $8^3=512$ candidate triples before the first-order sentence is checked; only six triples pass for the complete graph $K_3$. For $K_4$, there are $16^3=4096$ candidate triples and none passes. Distinguishing the range of candidates from the constraints on valid witnesses clarifies both full semantics for second-order logic and the verifier view of NP.

The appeal of full semantics for second-order logic is its literal reading of assertions about every subset or every relation. A first-order structure fixes the second-order ranges automatically, in contrast to Henkin semantics. That expressive force comes with a limitation: there is no effective, sound deductive system complete for all valid second-order logic sentences under full semantics for second-order logic. This limitation and the change of intended models motivating Henkin semantics are described at the start of ^[ref].

For a domain $V_{\lambda }$, an external functional graph with all its individual ordered pairs in $V_{\lambda }$ is therefore available, even if the whole graph does not belong to $V_{\lambda }$. More generally, a binary second-order relation variable can denote any external subset of $V_{\lambda }\times V_{\lambda }$; its ordered pairs need not themselves be elements of the individual domain. Having endpoints in the domain is what matters. This distinction between internal objects and externally available relations is essential when applying second-order logic to the cumulative hierarchy.

In Henkin semantics, a domain $D$ is accompanied by designated ranges ${\mathcal{H}}_k\subseteq \mathcal{P}(D^k)$ for second-order relation variables of each arity $k$. A formula $\exists R\phi (R)$ searches only ${\mathcal{H}}_k$, and $\forall R\phi (R)$ checks only ${\mathcal{H}}_k$. These ranges can be proper subcollections of the external power set. Keeping $D$ and its input relations fixed therefore need not fix the truth of a second-order logic sentence.

As a toy illustration of restricted quantification, take $D=\{a,b\}$ and unary range ${\mathcal{H}}_1=\{\varnothing ,D\}$. The sentenceis true under full semantics for second-order logic, but false with this selected range, because neither singleton is available. Likewise, on the complete graph $K_3$, the unary range $\{\varnothing ,D\}$ admits no witness for the second-order encoding of three-colorability, even though a usual proper vertex coloring exists. This toy range illustrates the truth definition only: it fails second-order comprehension for the formula $x=a$, and is not a model of a system requiring that comprehension instance.

Admissible Henkin semantics for a specified deductive system must satisfy its axioms, including its chosen second-order comprehension requirements or analogous closure conditions for predicate abstraction. Closure is relative to the permitted formulas and parameters, rather than a blanket property of every selected family. In particular, on a finite domain, allowing logical equality, individual parameters, all finite logical disjunctions, and comprehension for those formulas forces every finite-arity relation to be available: enumerate its tuples and disjoin the formulas naming them. Thus a proper restricted finite range cannot satisfy that entire scheme.

Treating each ${\mathcal{H}}_k$ as an additional sort, with an application relation between its members and $k$ individuals, translates this relational presentation into first-order logic with several sorts. Include axioms saying that predicates with the same members are equal, together with whatever second-order comprehension the system requires. This makes Henkin semantics useful for bringing first-order logic methods to reasoning about predicates; it does not license conclusions about all external relations.

Leon Henkin's Completeness in the Theory of Types, Journal of Symbolic Logic 15 (1950), pp. 81–91 develops general models and proves completeness for his typed deductive system. Its opening footnote 5 explicitly discusses closure under operations associated with formula formation. Henkin later described the discovery process in his ^[ref]; that later account is a historical recollection, distinct from the original publication.

A useful precise form of the Ehrenfeucht-Mostowski theorem is this: for an infinite structure $M$ and any linear order $I$, a model of $\mathrm{Th}(M)$ can be generated as a Skolem hull by distinct order indiscernibles $(a_i{)}_{i\in I}$. Every order automorphism of $I$ extends to an automorphism of that hull in the chosen Skolem language. One may first name all elements of $M$, giving an elementary extension containing the original structure. The generation and uniqueness assertions concern this specified expansion, not arbitrary automorphisms of its reduct.

Choose a Skolem expansion $M^{\ast }$: for each existential formula add a function selecting a witness whenever one exists. Introduce constants $c_i$ for $i\in I$. Take the theory of $M^{\ast }$, distinctness of these constants, and all equivalencesThe formulas here are in the fixed expanded language, without the newly added $c_i$ as extra parameters. If naming $M$, use its complete elementary diagram and allow those original names in the formulas.

Every finite fragment has a model by Ramsey's theorem. Only finitely many formulas and constants occur. Take a sequence of distinct elements of $M$. For each arity appearing, color the increasing tuples from this sequence by the finite vector of truth values of all formulas of that arity. Successive Ramsey thinning gives an infinite subset homogeneous for each of these finitely many colorings. Assign the finitely many constants in increasing order to distinct elements of this subset. This satisfies every displayed equivalence in the fragment; the original theory is satisfied because the underlying structure remains $M^{\ast }$. Compactness now gives a model of the full theory, with the required order-indiscernible sequence.

The substructure generated by the constants under the Skolem functions is elementary: any existential formula with parameters which are terms in the generators has its Skolem witness in that same hull. If $g$ is an order automorphism of $I$, defineIndiscernibility makes this well-defined, by applying it to the equation between any two term representations using the increasing tuple of all their indices. The same argument preserves every relation and function; $g^{-1}$ supplies the inverse. It is unique in the generated Skolem structure. This completes the Ramsey proof, rather than stopping at the existence of indiscernibles.

For simple typed set theory with atoms, use sorts $D_0,D_1,\dots$ and membership only from $D_i$ to $D_{i+1}$. A set predicate distinguishes sets from atoms, extensionality compares sets of the same positive type, and comprehension produces in type $i+1$ every subset of $D_i$ defined by a well-typed formula. Atoms have no members. First-order models use Henkin semantics; they are not required to have their next domain equal to the full external power set. Typical ambiguity is the schema $\varphi \leftrightarrow {\varphi }^{+}$ for each closed sentence, where every sort index in ${\varphi }^{+}$ is raised by one.

We show finite satisfiability of this entire typed theory with ambiguity. Choose a list of ranks ${\rho }_0<{\rho }_1<\cdots$ above $\omega$, spaced by at least two. For a finite increasing selection of ranks $r_{-1}<r_0<\cdots <r_m$, letwhere $S_i$ is the set of objects declared to be sets at type $i$. Membership from $D_i$ to $D_{i+1}$ is ordinary membership restricted to objects of $S_{i+1}=\mathcal{P}(D_i)$; all other type-$i+1$ objects are atoms. The spacing puts $\mathcal{P}(D_i)$ inside $D_{i+1}$. Thus comprehension and set extensionality hold exactly, and atoms have no typed members. There are infinitely many objects at every visible type, so any usual typed infinity requirement also holds.

The auxiliary rank $r_{-1}$ provides a uniform interpretation if a set predicate is allowed at type zero; no type-minus-one domain is used in the theory. This avoids artificially declaring all type-zero objects to be atoms, which would not be invariant under type-raising. If the language has no type-zero set predicate, simply ignore this auxiliary interpretation.

A finite set of ambiguity instances uses finitely many closed sentences of bounded highest type, say at most $m$. Color increasing $(m+2)$-tuples of ranks by their finite truth vector in the structure with visible domains $D_0,\dots ,D_m$ and the auxiliary preceding rank. Ramsey's theorem gives an infinite homogeneous rank set. Choose $m+3$ consecutive ranks from it and build the hierarchy on all these ranks. The first window evaluates each original sentence; shifting the window one place evaluates its uniform type-raise. Homogeneity makes the truth vectors equal. All finite typed axioms and the selected ambiguity instances therefore hold together. Choosing $m$ large enough covers every sort needed by the finite fragment. Many-sorted compactness, equivalently ordinary first-order compactness after encoding sorts, yieldsThis is a model existence argument in the ambient set theory; no equality of adjacent type cardinalities is claimed. The gaps between ranks supply atoms, and the ambiguity is about truth of sentences, not a bijection between domains.

For the Ehrenfeucht-Mostowski theorem, let $M$ be an infinite first-order structure and $I$ any linear order. Choose a full Skolem expansion $M^{\ast }$: add witness functions for existential formulas, repeat in the expanded languages, and take their union. We will construct a model of its theory containing distinct generators $c_i$, $i\in I$, forming an order-indiscernible sequence.

Adjoin the elementary diagram of $M^{\ast }$, the inequalities $c_i\ne c_j$ for $i\ne j$, and for every expanded-language formula $\varphi (x_1,\dots ,x_r)$ and every two increasing $r$-tuples of indices, the sentencesEvery finite subcollection is satisfiable in $M^{\ast }$. To prove this, choose a countably infinite sequence of distinct elements of $M$, and for each of the finitely many relevant arities color its increasing index tuples by the finite vector of truth values of the formulas of that arity. Repeated applications of the Ramsey's theorem give an infinite subsequence homogeneous for all these finitely many finite colorings. Interpret the finitely many mentioned $c_i$ by its elements in their index order. All indiscernibility and distinctness constraints hold, and the finite diagram fragment holds because the ambient structure is still $M^{\ast }$.

By compactness theorem, a model $N^{\ast }$ of the full enlarged theory exists. Its Skolem hull $H$ generated by the $c_i$ is elementary: whenever an existential formula with parameters in $H$ holds in $N^{\ast }$, its chosen witness function returns a value in $H$, so the Tarski-Vaught test applies. Its reduct is a model of $\mathrm{Th}(M)$. If the index order has size $\kappa$, the hull has size at most $\kappa +|L|+{\aleph }_0$, and it contains $|I|$ distinct generators.

Every order automorphism $h$ of $I$ induces the automorphismTo check well-definedness, write any two terms being compared over the same increasing list of their generators. Their equality is an expanded-language formula; indiscernibility of the order-indiscernible sequence preserves its truth under $h$. The same argument preserves each relation, and the term construction preserves the functions. Applying $h^{-1}$ gives the inverse. The extension is unique in the specified Skolem language since every hull element is a term in the generators; no uniqueness among all automorphisms of the reduct is being asserted. This proves the Ehrenfeucht-Mostowski theorem, including its usual automorphism consequence.

For simple typed set theory with atoms, use sorts $0,1,\dots$, predicates $S_i$ for sets, and typed membership from sort $i$ to sort $i+1$. Atoms have no members, extensionality compares sets, and every well-typed formula defines a set of the next sort. Typical ambiguity is the schema $\varphi \leftrightarrow {\varphi }^{+}$ for every closed typed sentence, where the superscript raises all types by one.

Here are concrete full typed models before imposing the ambiguity schema. Choose increasing natural numbers $n_{-1}<n_0<n_1<\cdots$ and setThe auxiliary $D_{-1}$ merely interprets the set predicate at the lowest sort. Define typed membership byThen the other objects of $D_{i+1}$ are atoms, regardless of their old membership. Every subset of $D_i$ has its representative in $S_{i+1}$, giving comprehension even for formulas with higher-sort quantifiers and parameters. Extensionality holds for the set representatives and atoms have no typed members. The rank gaps leave infinitely many atoms at each sort, and all sorts are infinite.

Consider finitely many ambiguity instances with unraised sentences ${\varphi }_1,\dots ,{\varphi }_t$, and choose a fixed window length $r$ sufficient to include every sort used and its auxiliary predecessor. Color every increasing $r$-tuple of natural numbers by the vector of truth values of these unraised sentences in its finite rank-window interpretation. There are only $2^t$ colors. The Ramsey's theorem gives an infinite homogeneous set. Choose $r+1$ successive points from it. The first $r$ points and last $r$ points have the same color, while the latter interpretation of ${\varphi }_j$ is exactly the former model's interpretation of ${\varphi }_j^{+}$. The auxiliary predecessor shifts too, so this remains true for sentences mentioning the lowest set predicate. Extend the chosen rank sequence arbitrarily to interpret the remaining sorts. This yields a model of typed set theory satisfying all the specified ambiguity instances.

Thus every finite subset of the typed axioms together with all ambiguity instances has a model. Applying multisorted compactness theorem givesThe final model satisfies first-order typed comprehension, with quantification over its own sorts and sets as in Henkin semantics.

The axiom of infinity excludes $V_{\omega }$ and all smaller stages, so the cardinal $\lambda$ is uncountable. Full semantics for second-order logic is decisive: every externally specified functional relation whose ordered pairs lie in $V_{\lambda }$ is an allowed class parameter, even if the relation itself is not an element of $V_{\lambda }$.

If $\mathrm{cf}(\lambda )=\mu <\lambda$, choose an external cofinal function $h:\mu \to \lambda$. Its graph is an allowed class parameter: each input, output and ordered pair has rank of a set below the infinite cardinal $\lambda$, which is a limit ordinal. The domain $\mu$ belongs to $V_{\lambda }$. The second-order form of Axiom schema of replacement would give its range as an element of $V_{\lambda }$. But a cofinal subset of $\lambda$ has rank of a set $\lambda$ and cannot belong to $V_{\lambda }$. Therefore $\mathrm{cf}(\lambda )=\lambda$.

If $2^{\theta }\ge \lambda$ for a cardinal $\theta <\lambda$, choice supplies an external surjection $q:\mathcal{P}(\theta )\to \lambda$. The domain belongs to $V_{\lambda }$ and the ordered pairs of its graph have ranks below $\lambda$. Applying Axiom schema of replacement to this external functional class would put its range, the ordinal $\lambda$, in $V_{\lambda }$, again impossible. Hence $2^{\theta }<\lambda$ for every $\theta <\lambda$.

ConsequentlyThese are exactly the defining conditions for a strongly inaccessible cardinal. This full second-order replacement rank obstruction would not follow from Henkin semantics, where the available class relations may exclude the external functions just used.

Second-order comprehension is a scheme asserting the existence of a second-order relation variable whose members are exactly the tuples satisfying a permitted formula:Here $R$ is not free in $\phi$, and the displayed individual and relation parameters are universally closed in each instance. Under full semantics for second-order logic, the selected external subset of $D^k$ is always available. Under Henkin semantics, the selected subset must lie in ${\mathcal{H}}_k$ for every allowed assignment of parameters. Different systems permit different formula classes: for example, arithmetical comprehension theory restricts comprehension to formulas without bound set variables, while still permitting set parameters. Consequently, the exact formula and parameter policy must accompany any claim that a restricted range satisfies second-order comprehension.

Second-order logic extends first-order logic by allowing existential quantification and universal quantification over second-order relation variables, as well as over individual objects. In the relational presentation used here, an individual variable $x$ ranges over a domain $D$, while a second-order relation variable $R$ of arity $k$ denotes a subset of $D^k$. Unary second-order relation variables denote subsets of $D$; binary ones denote binary relations. Presentations with function variables can instead describe their graphs by second-order relation variables, with first-order formulas requiring a unique output for every input.

For a graph with vertices $D$ and fixed graph adjacency $E$, the first-order sentence $\forall x\exists yE(x,y)$ says that every vertex has a neighbour. It selects individual vertices while $E$ retains its given interpretation. By contrast,selects an entire subset $P$ and says that it is a nonempty independent set. Here $P$ is a unary second-order relation variable, rather than a symbol in the input first-order signature. This particular property also has a simple first-order sentence on simple graphs; the example illustrates the change in what can be selected, rather than proving a separation in expressive power.

The usefulness of second-order logic is that one can describe a whole proposed solution, such as a graph coloring, and then impose local constraints on it. Syntax alone does not specify which proposed relations are available: full semantics for second-order logic permits all external subsets of $D^k$, whereas Henkin semantics supplies designated ranges. The second-order encoding of three-colorability makes this distinction concrete.

Objects have sorts $0,1,\dots$, with membership allowed only from sort $i$ to sort $i+1$. A set predicate distinguishes sets from atoms; atoms have no members, extensionality applies to sets, and every well-typed formula defines a set in the next sort by comprehension. First-order models may have only a specified collection of subsets, as in Henkin semantics. For a full finite-type model, take $D_i=V_{r_i}$ at widely separated increasing ranks, represent sets at level $i+1$ by $\mathcal{P}(D_i)\subseteq D_{i+1}$, and treat the remaining objects as atoms under typed membership.