An assignment in a first-order structure chooses a domain element for each variable. It determines the value of every first-order term and the truth of every first-order formula, once the interpretations of symbols are fixed. A first-order sentence has no free variables, so its truth is independent of the assignment in a first-order structure. Quantification changes the value assigned to the bound variable while retaining the other values.

An embedding of first-order structures is an injective function preserving function symbols and constants and both preserving and reflecting every relation symbol. Its image is a substructure. Satisfaction of an atomic diagram of a structure in an expansion gives such an embedding of first-order structures by sending each named element to its new interpretation; literal inclusion requires fixing the interpretations of those names.

In a first-order structure, an interpretation assigns a relation of the specified arity to each predicate symbol, a total function of the specified arity to each function symbol, and an element to each constant symbol. Evaluation of first-order terms and truth of logical formulas are then defined recursively. This specifies how symbols acquire their meanings on the underlying set.

A canonical first-order structure is generated by closed-term names: each element is the interpretation of a closed term. In a first-order language without function symbols this says each element is named by a constant. The constant-name convention for canonical first-order structures agrees with this one in the function-free setting. Logical equality identifies different names for the same element.

A function symbol is part of the syntax of a first-order language, with a specified finite arity. In a first-order structure it is interpreted as a function from the corresponding finite power of the domain into the domain. Applying it to the appropriate number of first-order terms forms another term. The symbol itself is distinguished from its interpretation in a particular structure.

A predicate symbol of arity $k$ is interpreted as a subset of the $k$th Cartesian power of a structure's domain. Applying it to $k$ first-order terms gives an atomic formula. In a singleton domain there is only one possible argument tuple at each arity, but a predicate may still be interpreted as either the empty relation or the full relation.

Replace an $n$-ary function by an $(n+1)$-ary graph predicate asserted to have exactly one output for each input tuple. A constant can be replaced by a unary predicate selecting one element. Term-value formulas in relational coding translate arbitrary terms, and formulas translate recursively through the logical operations. The original structures correspond bijectively to relational structures satisfying the graph axioms on the same carrier. Truth and consequences are preserved; arbitrary relations not satisfying those axioms do not represent functions.

In general, exchanging a universal and an existential quantifier changes a formula's meaning. A uniform witness satisfies a condition for every input, while a pointwise witness may vary with the input. For the equality relation on a two-element set, $\forall x\exists y(x=y)$ holds but $\exists y\forall x(x=y)$ fails.

An atomic formula or its logical negation. A first-order clause is a finite disjunction of first-order literals.

A quantifier prefix followed by a quantifier-free matrix. This does not itself eliminate existential quantifiers.

A quantified formula has a quantifier as its outermost formation: it is of the form $\forall x\theta$ or $\exists x\theta$. The quantifier binds the indicated variable occurrences according to the formation rules.

A representation by a set of first-order clauses, interpreted as their logical conjunction. General first-order formulas can be transformed by Skolemization and conversion to conjunctive normal form, preserving satisfiability in an expanded first-order signature.

In an expanded signature, Skolemization preserves equisatisfiability rather than equivalence under arbitrary interpretations of the new function symbols.

A first-order clause containing no variables. Its first-order terms are ground terms, so resolution between such first-order clauses reduces to propositional logic on the ground atoms.

For this cubic vector field, every non-axis trajectory has the first integral $I(x,y)=1/y-y/x^2$. Direct differentiation gives $\nabla I\cdot (\dot{x},\dot{y})=0$ where $xy\ne 0$. Equivalently the trajectories satisfy $x^2-y^2=C{x}^{2}y$. The axes are separate invariant trajectories, and the diagonals are the cases $C=0$. For each fixed finite $C$, approach to the origin forces $y^2/x^2=1-Cy\to 1$, so non-axis trajectories have diagonal limiting directions.

The origin is repelling in forward time. For $V=x^2+y^2$, $\dot{V}=2x^4+2x^2{y}^2+4y^4\ge V^2$, so every nonzero trajectory eventually exits any small disk. The zero Jacobian matrix at the origin leaves the linearized system constant, demonstrating why nonlinear terms are needed for this stability classification.

Multiply the ordinary differential equation by $f^{\prime }$ and integrate. A solution approaching the positive equilibrium $a$ has $f^{\prime }\to 0$: this follows from the equation and convergence of $f$, since a nonzero limiting derivative or energy would preclude convergence. Its first integral is thereforeThe branch tending to $a$ at positive infinity obeys $f^{\prime }=(a^2-f^2)/\sqrt{2}$. Separation yieldsThe constant solution is $A=0$. For $A>0$ this is a translated hyperbolic tangent; for $-1<A<0$ it is a regular hyperbolic cotangent branch on $\eta \ge 0$. The condition $A>-1$ excludes both an interior pole and a divergent value at the finite endpoint. The opposite sign in the first integral moves away from the positive equilibrium as $\eta$ increases, except at the constant solution.

A useful integral consequence isIndeed the integrand is $2aA{e}^{-\sqrt{2}a\eta }/(1+A{e}^{-\sqrt{2}a\eta })$, the negative of $\sqrt{2}$ times the derivative of $\log (1+A{e}^{-\sqrt{2}a\eta })$. An integral deficit can therefore fix the translation parameter uniquely, even when the differential equation and far value leave it free.

Using distinct fixed tags $t_1,\dots ,t_n$, encode a tuple $(a_1,\dots ,a_n)$ by the set $\{⟨t_i,a_i⟩:1\le i\le n\}$. Injectivity of the ordered-pair construction makes the unique member with first coordinate $t_i$ recover $a_i$. Thus a set can retain the order of a finite tuple when its entries are tagged, even if some coordinates coincide.

An ordered triple is a finite tuple with three ordered coordinates. Repeated coordinates are allowed; equality requires equality at each of the three positions.

For a nonempty finite sample, assign each distinct observed value its relative frequency. The observed values form the finite positive-mass support; the counts sum to the sample size, so the probabilities sum to one. Repeated observations increase the same outcome's mass rather than adding repeated support entries.

Given two finite probability distributions, assign the product of their probability masses to each ordered pair. The support is the Cartesian product of the two positive-mass supports. Distributivity gives ${\sum }_{x,y}{p}_1(x)p_2(y)=({\sum }_x{p}_1(x))({\sum }_y{p}_2(y))=1$. This is the joint distribution for independent coordinate outcomes; it is a construction from the marginals, not a claim that arbitrary jointly observed coordinates are independent.

Induct on the order of the finite p-group. Its center of a group is nontrivial unless the group itself is trivial. Quotient by the center to obtain a smaller finite p-group and lift a central series supplied by induction. Prepending the center gives a central series for the original group: the first term is central, and the remaining commutator-containment conditions are exactly the lifted quotient conditions. Hence every finite p-group is a nilpotent group. Since central factors are Abelian, every nilpotent group is also a soluble group.