Mathematical logic

Mathematical logic studies formal languages, formal proofs, model theory, computability theory, and the foundations of mathematics. It makes the rules of reasoning explicit enough that reasoning itself becomes an object of mathematics. Proof theory studies deductions; model theory studies interpretations in which statements hold.

Three questions organize the subject: is an expression a well-formed first-order formula, is it true in a specified first-order structure, and does it have a formal proof from specified axioms? These questions are distinct. For example, $\exists n(n+n=1)$ is a first-order sentence in an appropriate first-order language; it is false in the natural numbers but true in the rational numbers, with $n=1/2$.

The beauty of mathematical logic is that the same logical connectives and rules of universal quantification and existential quantification organize arguments across mathematics. Classical propositional logic uses two truth values; Intuitionistic propositional logic interprets logical implication through constructions on proofs, without unrestricted law of excluded middle. This proof-based framework is developed in Frank Pfenning, Natural Deduction, sections 1–3.

A logical formula is a finite expression constructed by the formation rules of a formal language. Propositional formulas combine propositional variables by logical connectives. First-order formulas additionally contain terms, atomic relations and quantifiers. A logical formula is a syntactic object; its truth is determined only after specifying a suitable interpretation and values for its free variables.

A logical variable is a symbol whose value is supplied by the semantics of a logical language. A propositional variable receives a truth value under a Boolean valuation. An individual variable of first-order logic receives an element of a structure under an assignment. These are different kinds of variable and should not be identified.

A logical fixed point is a formula or sentence equivalent to the result of applying a specified formula operation to itself. In arithmetic, self-reference is mediated by a Gödel number and the diagonal lemma, yielding a first-order sentence $G$ with a provable equivalence $G\leftrightarrow H(┌G┐)$. In modal logic, a modal formula $A$ satisfies $A\leftrightarrow F(A)$ modulo the chosen logic. A merely true semantic equivalence is weaker than a specified provable or canonical construction, so its hypotheses must be kept distinct.

A modal logic extends propositional connectives by operators such as $\square$ and its dual $◊A=\neg \square \neg A$. An interpretation determines their meaning: necessity, knowledge and formal provability lead to different axiom systems. In a relational semantics, $\square A$ holds at a world when $A$ holds at every accessible world. Provability logic interprets the box through arithmetically coded proofs.

Uniform substitution in modal logic replaces each occurrence of a first-order sentence letter by the same modal formula. Normal modal formal proof systems with axiom schemes are closed under this operation: substituted axioms remain instances, modus ponens is preserved, and necessitation commutes with substitution. Fresh auxiliary letters permit substituting a derived fixed point into fixed-point uniqueness theorems without changing other parameters.

Modal logic K4 extends the normal modal distribution axiom and necessitation rule by positive introspection $\square A\to \square \square A$. Its Kripke semantics uses transitive accessibility relations. The fixed point $B=\square (\square X\to X)$ satisfies $\square (B\to \square X)\to (B\to \square X)$ in this logic.

The normal distribution axiom says that a boxed implication and its boxed antecedent give the boxed consequent. Together with the necessitation rule, it permits boxed versions of propositional deductions. Under an arithmetic interpretation it is the internal modus-ponens condition among the Hilbert-Bernays-Löb derivability conditions. It does not permit dropping a box to assert the enclosed sentence.

A modal formula is built from propositional variables and logical constants using Boolean connectives and modal operators, such as the box operator. In provability logic, arithmetic realization replaces propositional letters by arithmetic sentences and interprets a box as the corresponding arithmetic provability assertion. Modal validity, theoremhood and truth under a particular arithmetic realization are distinct notions.

An occurrence of a propositional variable in a modal formula is modalized if it lies within the scope of a box operator. A variable occurs modalized in a formula when all its occurrences do. For example $p$ is modalized in $\square p\to q$, while $q$ is not. Fixed-point and uniqueness theorems for Gödel-Löb logic impose this syntactic condition on the variable being solved for.

Positive introspection says that a boxed assertion can itself be boxed. For an arithmetical provability predicate it is the third of the Hilbert-Bernays-Löb derivability conditions: provability of $A$ implies provability of the assertion that $A$ is provable. It follows from formalized Sigma-1 completeness when provability assertions are Sigma-1. It is not the reflection principle $\square A\to A$.

The necessitation rule permits boxing a theorem in a modal proof system. It does not permit boxing an arbitrary temporary assumption. Under an arithmetic interpretation, it uses the external first of the derivability conditions: an actual proof of $A$ supplies a proof that $A$ has a proof. This distinction matters when proving the Internal form of Löb's theorem.

Provability logic studies modal principles valid when $\square A$ is interpreted by an arithmetical provability predicate. The distribution axiom corresponds to formalized modus ponens rule, necessitation corresponds to verification of actual proofs, and the Löb axiom is the Internal form of Löb's theorem. The standard system capturing these principles is Gödel-Löb logic.

The Gödel-Löb logic has propositional tautologies, $\square (A\to B)\to (\square A\to \square B)$ and $\square (\square A\to A)\to \square A$ as axiom schemes. Its rules are modus ponens rule and the necessitation rule; uniform propositional substitution is built into the schemes. Under an arithmetic realization, each axiom and each rule preserves provability in a theory with the Hilbert-Bernays-Löb derivability conditions and diagonalization. This proves arithmetic soundness by induction on derivations; it is distinct from claiming that every true arithmetic sentence is provable.

The Löb axiom $\square (\square A\to A)\to \square A$ over normal modal logic already implies $\square X\to \square \square X$. Put $C=\square X\wedge X$. Distribution gives $\square C\to \square X$, hence $X\to (\square C\to C)$. Necessitation and distribution give $\square X\to \square (\square C\to C)$; the Löb axiom gives $\square C$, which implies $\square \square X$.

A formula provably equivalent to a boxed formula satisfies $F\to \square F$ in GL. The displayed fixed point then gives both $\square \square F$ and $\square \neg \square F$ under $F$, hence $\square \perp$. Boxed explosion proves the reverse implication. Under arithmetic realization this is a formal inconsistency statement; Sigma-1 soundness excludes its provability, while second incompleteness excludes provability of its negation.

If every occurrence of $p$ in $X(p)$ lies under a box, Gödel-Löb logic has a formula $F$ without $p$, using only the other letters of $X$, satisfying the displayed equivalence. Write $X(p)=H(\square C_1(p),\dots ,\square C_m(p))$ using the outermost boxes that contain $p$, so $H$ has no $p$. Solve $q_i\leftrightarrow \square C_i(H(q_1,\dots ,q_m))$ by simultaneous boxed fixed-point elimination in GL. If the solutions are $Q_i$, then $F=H(Q_1,\dots ,Q_m)$ works by replacement of provably equivalent formulas.

In Gödel-Löb logic, the one-variable identity $\square C(\top )\leftrightarrow \square C(\square C(\top ))$ solves a boxed equation with a formula omitting its unknown letter. A finite simultaneous system can be solved by elimination. First solve its last equation with the other unknowns treated as parameters, substitute that formula into the preceding equations, and apply induction. Substituting the resulting solutions back into the last formula completes the system. This construction introduces no new parameter letters.

Let $U=\square Y(\top )$ and $V=\square Y(U)$. Boxed replacement gives $\square U\to (U\leftrightarrow V)$, and positive introspection gives $U\to V$. For the reverse implication rewrite it as $V\to (\square U\to U)$, necessitate, use $V\to \square V$, and apply the Löb axiom to obtain $V\to \square U\to U$. This explicit one-variable construction needs no reflection axiom.

The Löb axiom gives $\square F\to \square q$. The tautology $q\to F$, necessitated and distributed, gives $\square q\to \square F$. Thus $\square F\leftrightarrow \square q$, and replacing the antecedent in $\square F\to q$ gives exactly $F$. Setting $q=\perp$ produces a negative-provability fixed point, provably equivalent to $\neg \square \perp$.

Map propositional letters to arithmetic sentences, map falsity to a refutable sentence, commute with implication and interpret $\square$ by an arithmetical provability predicate. Propositional axioms remain theorems. The K axiom uses the second of the derivability conditions, and the Löb axiom uses the Internal form of Löb's theorem. Modus ponens rule is preserved directly, and the necessitation rule uses the first derivability condition. Induction on a GL proof therefore proves the displayed soundness implication for Peano arithmetic with the stipulated provability predicate.

A modal operator forms a new formula from a formula, such as $A\mapsto \square A$. In provability logic, it represents an assertion that a proof of $A$ exists, rather than an assertion that $A$ is true. A box is not interchangeable with an unboxed formula.

A family of logics describing classes of individuals and relationships between individuals, with restricted constructors chosen to support reasoning.

The assumption that distinct individual names denote distinct domain elements. Standard ALC semantics does not impose it; Herbrand interpretations do treat distinct ground terms as distinct elements.

A description logic concept is satisfiable with respect to a TBox if some model of that TBox interprets the concept as a nonempty set.

A rule-oriented description logic fragment designed for translation to function-free Horn rules, allowing constraints but excluding existential witness generation in rule conclusions. In an equivalence, each direction must meet the relevant restrictions. ^[ref]

The description logic generated by atomic concepts, $\top$, conjunction and existential restrictions. Some conventions also allow $\perp$; that extension is distinguished here as EL with bottom. Without $\perp$, every concept is satisfiable with respect to every EL TBox.

EL extended with $\perp$, allowing disjointness and unsatisfiable concepts. Concept satisfiability with respect to general TBoxes is P-complete.

The description logic with atomic concepts, top and bottom, Boolean concept constructors, and existential and universal restrictions on description logic roles.

A concept satisfiability procedure that expands concept labels into a graph, branches on disjunctions, creates witnesses for existential restrictions, propagates universal restrictions along existing edges, and tests for a tableau clash. General TBoxes require global constraints and a termination device such as direct blocking in description logic.

A test that stops further witness generation at a node when an appropriate earlier ancestor already represents its required pattern of labels. The exact test depends on the logic and tableau calculus. An isolated root has no ancestor and is not directly blocked.

An explicit contradiction in a node label, such as both $A$ and $\neg A$, or $\perp$. Opposite universal restrictions alone cause no clash when there are no successors.

A collection of assertions about individuals, such as $A(a)$ and $R(a,b)$, interpreted together with a TBox.

A collection of terminological axioms, including general concept inclusions, constraining the meanings of description logic concepts and description logic roles.

Rewriting suitable general axioms into definitions or primitive inclusions that can be processed when an atomic label is encountered. For example, $A\sqcap B⊑\perp$ can be absorbed as $A⊑\neg B$.

Substitution of acyclic concept definitions into expressions to be tested. Primitive inclusions require care: $A⊑D$ can be represented using a fresh name $A_0$ by $A\equiv A_0\sqcap D$, but is not equivalent to $A\equiv D$.

An axiom requiring every instance of the description logic concept $C$ to be an instance of $D$. It holds throughout the domain, not just at named individuals.

A binary relation on individuals used by description logic restrictions such as $\exists R.C$ and $\forall R.C$.

A unary description interpreted as a subset of the domain. Atomic names can be combined using the constructors of the chosen description logic.

Two sentences or theories are equisatisfiable when one has a model if and only if the other has a model. They need not be true in the same interpretations or even use the same signature.

A family of formal languages for assertions involving time or successive states, including linear temporal logic and computation tree logic.

A branching temporal logic whose operators quantify over paths in a transition system from a state. In particular, $AG\Phi$, also written $\forall \square \Phi$, holds at $s$ when every infinite path in a transition system from $s$ satisfies $\Phi$ at every position, including its initial position.

A temporal logic interpreted along infinite paths in a transition system. At position $i$, $X\alpha$ requires $\alpha$ at $i+1$, $F\alpha$ requires it at some $j\ge i$, and $G\alpha$ requires it at every $j\ge i$. Strong until and weak until express conditions that hold up to a later event. A system satisfies a specification when all relevant initial paths in a transition system satisfy it.

In linear temporal logic, $\alpha \mathrm{W}\beta$ means $(\alpha \mathrm{U}\beta )\vee G\alpha$. Thus it permits the left operand to hold forever without the right operand ever becoming true, unlike strong until.

In linear temporal logic, $\alpha \mathrm{U}\beta$ holds at position $i$ exactly when some $j\ge i$ satisfies $\beta$ and every position $k$ with $i\le k<j$ satisfies $\alpha$. The witness $j$ must exist. The case $j=i$ imposes no condition on $\alpha$.

The linear temporal logic operator $X\alpha$, true at position $i$ of a path in a transition system exactly when $\alpha$ is true at position $i+1$. Thus $XX\alpha$ tests two positions ahead.

An inference rule licenses a conclusion from specified premises, possibly with side conditions. A derived inference rule is justified by a logical derivation using the primitive inference rules; using it subsequently abbreviates that logical derivation.

A derived inference rule abbreviates a logical derivation from the primitive inference rules. Its use retains the assumptions and side conditions required by that logical derivation; proving the abbreviation once allows subsequent proofs to use the rule without expanding every intermediate line.

A logical derivation is a finite application of explicitly specified inference rules to premises or temporary assumptions. In natural deduction, which assumptions remain open is part of the logical derivation: a conclusion reached inside a temporary subproof cannot simply be used outside it.

A sequent $\Gamma ⊢A$ records that the formula $A$ is derivable with undischarged assumptions drawn from $\Gamma$. In natural deduction, a temporary assumption contributes to $\Gamma$ only until an appropriate discharge rule closes its scope.

A propositional formula or first-order formula is in negation normal form when its negations occur only directly before atomic formulas, and its other logical connectives are conjunction and disjunction, together with quantifiers in the first-order case. Remove implications using $P\to Q\equiv \neg P\vee Q$, then push negations inward using De Morgan's laws, double-negation cancellation, andIn particular, negating an implication gives $P\wedge \neg Q$, so its antecedent retains its original sign after the outer negation has been pushed through.

A choice of a domain and meanings for the symbols of a formal language, used to evaluate its sentences. The same sentence can have different truth values under different interpretations, unless it is valid under every admitted interpretation.

Reasoning in which the conclusion follows from the premises by valid inference. A valid argument need not have true premises; soundness additionally requires their truth.

A solution exists when at least one object satisfies all the stated conditions. In first-order logic, this is expressed by existential quantification. Uniqueness additionally requires that any two solutions are equal.

A solution is unique when any two objects satisfying the stated conditions are equal. This is an at-most-one assertion; existence is a separate requirement. A common proof assumes two solutions, subtracts their equations, and proves that their difference vanishes. For a linear differential equation this turns the task into a homogeneous problem with zero boundary or initial data.

Proof theory studies formal proofs and the deductive systems that produce them. It examines which conclusions follow from axioms, how proofs can be transformed, and what those transformations reveal about the chosen logic. Natural deduction organizes a proof through introduction and elimination rules for logical connectives and quantifiers.

A Hilbert proof system specifies axiom schemes and inference rules, commonly including modus ponens. A formal proof is a finite sequence of axiom instances, permitted assumptions and conclusions obtained from preceding lines by those rules. Soundness and completeness compare this syntactic derivability with semantic validity or semantic entailment. These properties concern the particular chosen axioms and rules.

One presentation of classical propositional logic uses the schemes $A\to (B\to A)$, $(A\to (B\to C))\to ((A\to (\neg B\to C))\to (A\to C))$, and $(A\to B)\to (A\to (\neg B\to C))$, together with modus ponens rule and the case rule from $A\to B$ and $\neg A\to B$ to $B$. Its deduction theorem for propositional logic follows by induction on logical derivations: conditional modus ponens handles a modus ponens rule line, and the second scheme handles a case-rule line.

Take precisely the propositional tautologies as axioms and supply no inference rules. A one-line proof then establishes exactly the valid propositional formulas, so this calculus is sound and complete for theoremhood. Its axiom set is decidable by finite truth tables. This construction does not by itself give strong completeness for consequence from arbitrary assumptions.

An inference rule deriving a clause from two clauses containing complementary literals. In propositional logic the displayed rule eliminates the atom $A$. For first-order clauses, complementary atoms can first be made identical by a suitable first-order substitution.

A rule that combines first-order clauses by unifying complementary first-order literals and retaining the other literals under the resulting first-order substitution. Completeness requires the appropriate calculus and search conditions.

A family of resolution calculi for first-order Horn clauses. A selection function chooses either the positive head atom alone or a nonempty set of body atoms. Permitted inferences respect those choices; fair saturation is refutationally complete. Function symbols need not be excluded, so completeness does not by itself guarantee termination. ^[ref]

The use of resolution on ground clauses. A finite refutation ends in the empty ground clause and establishes unsatisfiability of the chosen ground instances. Herbrand's theorem explains the completeness of searching for such refutations for universal equality-free first-order clauses.

An axiom is a sentence admitted as a starting assumption of a formal theory. An axiom schema specifies a collection of such sentences, usually one for each formula of an allowed form. A model of a first-order theory satisfies all its axioms; a relative consistency construction can show that the other axioms do not imply a particular omitted one.

An axiom set is the collection of formulas available as axioms in a specified formal proof system. It may be finite or infinite, or specified by an axiom scheme.

For an independent axiom set, semantic entailment of any one axiom from the remaining axioms fails. By the completeness theorem, this is equivalent to no member being formally derivable from the others in a complete calculus. To establish independence it suffices to give, for each axiom, a first-order structure satisfying all the other axioms and failing that one.

The usual associative, identity, two-sided inverse and commutativity axioms form an independent axiom set. A three-element commutative unital operation with self-inverses can fail associativity; a constant-zero operation can satisfy the other three axioms while failing the identity condition; natural-number addition fails the inverse condition; and a noncommutative group fails commutativity. Each example must be checked against all three retained axioms.

A mathematical definition fixes the meaning of a term or symbol using previously specified concepts. A definition by a universal property can still require a mathematical proof that an object with that property exists. For example, the definition of a product in a category specifies its mapping behavior, while existence is a further question about that category.

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.

A second-order relation variable of arity $k\ge 1$ can be assigned a subset of the $k$-fold Cartesian product $D^k$; its application $R(x_1,\dots ,x_k)$ is true exactly when the tuple $(x_1,\dots ,x_k)$ belongs to that subset. Arity is the number of arguments, so a unary second-order relation variable is a predicate on individual objects. For a finite set $D$ of cardinality $n$, there are $n^k$ possible tuples and $2^{n^k}$ possible relations under full semantics for second-order logic. A relation is encoded by $n^k$ membership bits once the objects have been numbered; the number of possible witnesses can be exponential even when each witness has a short encoding.

An existential second-order logic sentence has the formwhere each $R_i$ is a second-order relation variable of fixed finite arity $k_i$ and $\phi$ is a first-order sentence over the input first-order signature expanded by the $R_i$. The first-order sentence may contain both universal quantification and existential quantification over individuals; only the outer quantification over second-order relation variables is required to be existential. Under full semantics for second-order logic, truth means that some expansion by witness relations satisfies $\phi$.

For a fixed existential second-order logic sentence on a domain of cardinality $n$, the witnesses need ${\sum }_{i=1}^m{n}^{k_i}$ membership bits. The arities and the number of witnesses are constants because the sentence is fixed. After guessing those bits, a verifier evaluates the fixed first-order sentence by enumerating assignments to its finitely many individual variables, taking polynomial time. In the second-order encoding of three-colorability, the three witnesses require $3n$ bits, and the edge constraints can be checked over at most $n^2$ ordered vertex pairs. This is the logical form of the NP principle that a positive answer has a short complexity certificate.

The fixed-sentence qualification matters: it is the input first-order structure that varies, rather than an arbitrarily large formula supplied with each input. Fagin's theorem states the converse as well: every isomorphism-invariant NP property of finite relational first-order structures has such a description. The coloring example uses only unary second-order relation variables; the general theorem allows any fixed finite arities.

Represent a finite simple graph by a domain $D$ of vertices and a symmetric, irreflexive binary relation $E$ for graph adjacency. Introduce three unary second-order relation variables $C_1,C_2,C_3$, one for each fixed named colour. Define the following abbreviations for first-order formulas in this expanded first-order signature:Then the existential second-order logic sentenceasserts that every vertex receives exactly one of the three colours and adjacent vertices receive different colours. The first clause gives coverage and pairwise disjointness of the three subsets; the second makes each subset an independent set. Empty colour classes are allowed, so ${\Phi }_3$ expresses existence of a proper vertex coloring using at most three colours.

For the complete graph $K_3$ on the fixed vertices $a,b,c$, one witness is $C_1=\{a\}$, $C_2=\{b\}$, $C_3=\{c\}$. Each vertex satisfies exactly one predicate, and each of the three edges joins different predicates. Every valid witness assigns different colours to all three vertices; there are $3!=6$ witness triples with these fixed vertex labels and fixed named colours. We are counting assignments, without identifying them under colour permutations or graph isomorphisms. For the complete graph $K_4$, the pigeonhole principle forces two of its four vertices to share a colour, and those vertices are adjacent. Thus it has no witness triple. This calculation illustrates a complexity certificate without requiring the reader to reconstruct a machine computation.

Reproduce the diagram by running python ../second-order-coloring-witness.py from the repository's _media directory. The script checks all witness triples for these two complete graphs before drawing them.

Fix a finite relational first-order signature $\tau$, and let $\mathcal{K}$ be a class of finite nonempty $\tau$-first-order structures closed under isomorphism. Fagin's theorem states that $\mathcal{K}$ is definable by one existential second-order logic sentence under full semantics for second-order logic if and only if its language of standard finite encodings belongs to NP. A standard encoding numbers the domain $\{0,\dots ,n-1\}$ and lists membership bits for each input relation, together with $n$; take an explicit encoding whose length is at least $n$. The encoding language contains all numbered copies of members of $\mathcal{K}$, with malformed encodings rejected. The isomorphism condition makes membership a property of the structure rather than an arbitrary choice of labels. Changing between the usual explicit encodings preserves the NP characterization by polynomial time translations.

The forward direction is the witness-and-verifier calculation in existential second-order logic. For the reverse direction, the guiding idea is to encode an accepting nondeterministic computation using second-order relation variables: fixed-length tuples of domain elements index enough time steps and storage positions for a polynomial time computation. A first-order sentence checks the initial input, legal transitions, and acceptance. The number of tuples grows with the input, although the checking sentence stays fixed. No total order must be supplied as part of the input first-order signature: an auxiliary total order can itself be existentially guessed and constrained by a first-order sentence. Isomorphism invariance ensures that a change of this auxiliary numbering does not change membership in $\mathcal{K}$.

The second-order encoding of three-colorability is a small instance of the forward direction. The beauty of Fagin's theorem is the complete correspondence: the computational class NP can be characterized by the shape of a logical description, without mentioning a particular machine in the statement. The scope is finite relational first-order structures and fixed sentences; it is not a claim about deciding arbitrary second-order logic sentences or about arbitrary infinite domains.

Ronald Fagin published the result in Generalized First-Order Spectra and Polynomial-Time Recognizable Sets, SIAM-AMS Proceedings 7 (1974), pp. 43–73, Section 4. The original paper frames the correspondence using classes of finite expansions and their encodings. Fagin's author-maintained publication list explains that the abstract in the available copy was added in 2019; its modern summary should therefore not be mistaken for part of the 1974 printing.

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.