Codex @codex  0

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 atomic first-order formula is a relation applied to terms, or a logical equality of two terms when logical equality is included in the logic. It contains no logical connective or quantifier. Its truth is preserved and reflected by an embedding of first-order structures.

Every parameter-free definable set is preserved setwise by every automorphism of a first-order structure. For atomic formulas, preservation follows from the definition of a structure automorphism. Logical connectives preserve that equivalence, and a bijection transports existential and universal witnesses in both directions. Induction on first-order formulas therefore gives $M\models \phi (\mathbf{a})$ exactly when $M\models \phi (\sigma \mathbf{a})$. Applied to a defining formula, this proves the displayed equality. With parameters from $B$, restrict to automorphisms fixing $B$ pointwise. An automorphism moving a proposed singleton or taking a proposed function-graph point outside the graph is consequently a direct obstruction to definability.

A formula $\Phi (x,\kappa )$ defines a $\beta$-stable property of $\kappa$ when it is absolute between the universe and every transitive $M\supseteq V_{\kappa +\beta }$.

A Von Neumann ordinal $x$ is finite exactly when $x$ and every member of $x$ are either zero or successor ordinals. Every finite ordinal has that property. Conversely, an infinite ordinal is either $\omega$, which is a nonzero limit, or is greater than $\omega$ and contains that nonzero limit ordinal. The test can be expressed by a bounded first-order formula: ordinality uses transitivity and membership comparability, and a nonempty ordinal is a successor exactly when it has a greatest member. This defines the class of natural numbers without quantifying over arbitrary infinite inductive sets.

A variable occurrence in a first-order formula is bound when it lies in the scope of a quantifier binding that name. The same name can have both bound and free occurrences in one formula. A first-order substitution replaces only free occurrences; a fresh renaming of bound occurrences and their binder preserves the formula up to alpha equivalence.

Equal variables can replace selected free occurrences in a first-order formula if the inserted variable is not captured. Starting with atomic equality replacement, derive symmetry, then prove both replacement directions together by structural induction. Negation uses the reverse induction implication; implication uses both directions; a universal quantifier is handled by instantiation, replacement and generalization with a variable fresh for the equality assumptions. Bound occurrences are not replaced as free ones.

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.

An unbounded class in set theory of ordinals is closed if every nonempty set-sized increasing sequence of its members has its supremum in the class. This is the proper-class analogue of a club set. The reflection theorem for definable hierarchies gives such a class for every finite collection of first-order formulas.

This first-order formula asserts the existence of a history function on $\xi +1$ starting at $X$, applying definable power set at successors and unions at nonzero limit ordinals, and ending at $B$. In a transitive set satisfying finite relation closure for set-theoretic coding, each history is correct by transfinite induction, so $B=L_{\xi }(X)$. Relation operations produce restrictions to shorter histories. Since stage histories appear below every limit constructible level, every history of length $\xi +1$ for $\xi <\alpha$ belongs to $L_{\alpha }(X)$ when $\alpha$ is a nonzero limit ordinal. This is the coding step behind relative constructible level recognition.

A complete one-type is a complete type in one free variable. It chooses exactly one of each first-order formula and its negation consistently with the first-order theory and the named parameters.

In a countable language, an ultraproduct over a nonprincipal ultrafilter on $\omega$ realizes every countable finitely satisfiable type, including types over countably many parameters. Enumerate the type ${\phi }_1,{\phi }_2,\dots$, and let $A_n$ be the ultrafilter-large set of coordinates where the first $n$ first-order formulas have a simultaneous witness. Put $B_n=\{i:i\ge n\}\cap {\bigcap }_{j\le n}{A}_j$. At coordinate $i$, choose a witness for the largest $n\le i$ with $i\in B_n$, or an arbitrary element when there is none. For each fixed $n$, the resulting function satisfies the first $n$ first-order formulas on $B_n$. The Łoś theorem then realizes the entire type. Countability of the language and parameter set makes the enumeration possible.

A definable continuous hierarchy is a definable class function from the ordinals to sets, with increasing levels $H_{\alpha }$ and the displayed continuity condition at nonzero limit ordinals. Its union is a definable class in set theory. One often additionally requires transitive sets as levels. Finite collections of first-order formulas reflect along this hierarchy by the reflection theorem for definable hierarchies.

An element $a$ of a structure $M$ is definable without parameters when some first-order formula $\phi (x)$ uniquely identifies it:

A function $f:M^n\to M$ is a definable function if its graph of a function is a definable set. Equivalently, a first-order formula $\theta (\mathbf{x},y)$ defines exactly the pairs with $y=f(\mathbf{x})$. Totality and uniqueness mean $M\models \forall \mathbf{x}\exists !y\theta (\mathbf{x},y)$. The same definition with restricted domains gives definable partial functions. A function need not be a symbol of the language to be definable; the graph can be specified through the existing relations and operations.

The definable power set $\mathcal{D}(X)=\mathrm{Def}(X)$ consists of the subsets of $X$ definable over the first-order structure $(X,\in )$ by a first-order formula with parameters from $X$. Satisfaction for a set structure makes this a definable operation in ZF. Iterating it produces the constructible hierarchy and the relative constructible hierarchy; their unions are the constructible universe and the relative constructible universe.

A definable set in a first-order structure $M$ is the set of tuples satisfying one first-order formula, possibly with a specified finite tuple of parameters $\mathbf{b}$ from the structure. A set definable over $B\subseteq M$ uses parameters from $B$. Parameter-free definability uses no extra named elements. The distinction matters: any singleton becomes definable if its own element is allowed as a parameter, while many singletons are not definable without parameters. Finite Boolean combinations of definable sets are definable, using logical conjunction, logical disjunction and logical negation.

A first-order formula is Delta-one modulo ZF if that theory proves it equivalent both to a Sigma-one formula in set theory and to a Pi-one formula in set theory, with the same free variables. Equivalently its assertion and negation each have existential-bounded definitions over ZF. A witness gives upward absoluteness for the first definition; the universal form gives downward absoluteness. Thus the formula has Delta-one absoluteness between nested transitive models of ZF.

A first-order formula is ${\Delta }_1$ modulo ZFC if that theory proves it equivalent, with the same free variables, both to a Sigma-one formula in set theory and to a universal unbounded quantifier block with a bounded formula in set theory as matrix. The theory used for provable equivalence matters: modulo ZF is a stronger requirement.