First-order logic

First-order logic permits quantification over elements of a structure while its nonlogical symbols describe operations, constants, and relations.

A Hilbert-style calculus specifies axiom schemes and a small collection of inference rules, typically implication elimination and universal generalization. Equality and quantifier schemes include substitution and free-variable side conditions. Proofs are finite syntactic derivations; validity is separately defined using structures and assignments. A context-sensitive presentation restricts generalization by its actual undischarged assumptions.

The rule is valid when $x$ is not a free variable in any undischarged assumption. Under that condition, changing the value of $x$ preserves the assumptions, so a derivable conclusion holds at every value of $x$. Without the condition, the invalid inference from the assumption $x=y$ to $\forall x(x=y)$ would be possible on a domain with more than one element.

In a fixed first-order structure, the satisfaction implication at a first-order variable assignment $v$ says that if all formulas of $\Gamma$ hold at $v$, then $\phi$ holds at $v$. Semantic consequence requires that implication in every relevant structure and assignment. The assignment's codomain belongs to its structure; different domains are not silently assigned one common map. When all formulas are first-order sentences, assignments do not affect any of their truth values.

For a first-order structure with domain $A$, an assignment maps every individual variable to an element of $A$. It extends recursively to first-order terms using the interpreted functions. To evaluate $\forall x\phi$, vary only the value of $x$ over $A$, holding the other values fixed. The truth value of a first-order formula depends only on its free variables; a first-order sentence is therefore independent of the assignment.

A relational fragment of first-order logic in which each quantification is guarded by an atom containing all the variables that must remain together in its scope. The usual fragment excludes nonconstant function symbols.

A function-free implication between conjunctions of positive atomic formulas, allowing existentially quantified witnesses in its conclusion. Standard tuple-generating dependencies do not have disjunctive heads or negative constraints.

The set of all ground terms over a first-order signature $\sigma$. Add a fresh constant if the first-order signature has none, so that this domain is nonempty. A constant $a$ and unary function $f$ give the Herbrand universe $\{a,f(a),f(f(a)),\dots \}$.

The set of all ground atoms formed using a Herbrand universe and the signature's predicates.

A first-order structure whose domain is the Herbrand universe, with constants denoting themselves and function symbols acting by syntactic term formation. Its predicates are specified by assigning truth values to ground atoms. With first-order equality, ordinary equality of syntactic terms imposes additional restrictions; more general term models may require quotienting by a congruence.

Equivalently, the predicate meanings of a Herbrand interpretation correspond to a subset of its Herbrand base.

A Herbrand structure satisfying the specified first-order sentences or first-order clauses.

For a satisfiable equality-free universal logical conjunction of Horn clauses, intersecting the sets of true ground atoms of its Herbrand models gives another Herbrand model, contained in every one of them. A ground atom is true in this least Herbrand model exactly when it holds in every Herbrand model. Positive existential sentences are true in the least Herbrand model exactly when they follow from the Horn clauses; allowing negated atoms makes this equivalence fail. For example, the least Herbrand model of $\forall x(P(x)\to Q(x))$ over a single constant $a$ makes both predicates empty and satisfies $\exists x\neg P(x)$, whereas the first-order structure making both predicates universal is a countermodel to that consequence.

A set of universally quantified equality-free first-order clauses is unsatisfiable if and only if some finite set of its ground instances is propositionally unsatisfiable. Equivalently, such a set is satisfiable if and only if it has a Herbrand model. General first-order sentences can first undergo Skolemization. A fresh constant is added if needed to make the Herbrand universe nonempty; first-order equality requires its corresponding equality treatment.

A finite logical disjunction of atomic first-order formulas or their negations, normally understood to have all its free variables universally quantified. An empty logical disjunction is false. A Horn clause has at most one positive atom.

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.

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 interpretation, together with an assignment to any free variables, in which all premises of a proposed inference hold and its conclusion fails. By soundness of the inference rules, a countermodel proves that the inference cannot be derived. For example, on $\{0,1\}$ with $P=Q=\{0\}$ and $x=0$, the formula $\forall y(P(y)\to Q(y))$ is true but $P(x)\to \forall yQ(y)$ is false. A pointwise assumption about $x$ cannot justify unrestricted universal quantification.

A single witness working for every object supplies a witness for each object individually. Eliminate the outer existential with a fresh witness, instantiate the universal at an arbitrary object, and introduce the required existential. Generalization can occur either before or after closing the witness scope, provided the eigenvariable condition holds in the corresponding contexts. The converse fails on a two-element domain with $R(x,y)$ interpreted as equality: each object has itself as a witness, but no object works for both.

For a fixed positive integer $k$, the displayed first-order logic sentence says that exactly $k$ distinct elements satisfy $R$. The pairwise inequalities and positive instances give at least $k$ witnesses; the universal exhaustiveness clause gives at most $k$. Additional parameters can remain fixed inside $R$. For $k=0$, use $\forall y\neg R(y)$ instead. Omitting distinctness or exhaustiveness changes exactly to a weaker counting condition.

For a fixed finite list of unary predicates, a unary predicate type specifies whether each predicate holds of an element. With $k$ predicates there are $2^k$ possible truth value patterns; a first-order structure may realize any subset of them. The notation $P^1=P$, $P^0=\neg P$ makes each pattern a quantifier-free formula.

The displayed first-order sentence requires a domain with at least $2^k$ elements without using logical equality. Distinct patterns disagree on some predicate, so a single element cannot witness both. Conversely, a domain consisting of the $2^k$ binary strings of length $k$, with $P_i$ selecting strings whose $i$th bit is one, realizes every pattern. More generally, requiring any $m$ distinct unary predicate types forces at least $m$ distinct elements.

To perform a first-order substitution, first rename each conflicting bound variable to a fresh name, then replace the designated free occurrences. The fresh names must avoid the formula's relevant free names and all names in the inserted first-order term. For instance, substituting $f(u,t)$ for $z$ in $\exists tQ(z,t)$ requires renaming the binder, producing $\exists sQ(f(u,t),s)$ rather than $\exists tQ(f(u,t),t)$. The latter would change the intended meaning by capturing $t$.

A first-order term $\tau$ is free for substitution for a variable $z$ in a first-order formula when no free variable of $\tau$ becomes bound after replacing a free occurrence of $z$. Equivalently, at every free occurrence to be replaced, none of its enclosing quantifiers binds a variable appearing in $\tau$. The test depends on occurrences and scopes, not merely on which variable names appear anywhere in the formula.

Replacing every free occurrence of variable $z$ in a first-order formula by a first-order term $\tau$. Bound occurrences of $z$ are left alone. The operation requires either that $\tau$ be free for substitution at those occurrences or that conflicting bound variables first be renamed, as in capture-avoiding first-order substitution.

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.

The convention that ground facts not present in the current representation are false. In a basic STRIPS state, listing the true facts therefore determines a complete interpretation for its ground facts. This convention differs from a knowledge base in which an absent assertion is simply unknown.

A quantifier binds a free variable in a first-order formula and specifies how its truth depends on elements of a first-order structure: universal quantification $\forall$ requires every element, while existential quantification $\exists$ requires at least one.

The fragment $L^k$ permits at most $k$ distinct variable names, but allows bound names to be reused. It can contain formulas of arbitrarily large quantifier depth. On a linear order, alternating two variable names can express an increasing chain of any prescribed finite length.

On a finite linearly ordered structure with an equivalence relation, the formula $\forall y(y<x\to \neg E(y,x))$ selects exactly the least element of each equivalence class. Variable-recycling counting therefore expresses any prescribed lower bound on the number of classes. The order and equivalence-relation axioms use three variable names. Finiteness matters: densely interleaved infinite classes need not have least elements.

For a formula $\varphi (x)$ in $L^k$, $k\ge 2$, with only $x$ free, define $C_1^x=\varphi (x)$ and $C_{m+1}^x=\varphi (x)\wedge \exists y(x<y\wedge C_m^y)$. Obtain the superscript-$y$ formula by globally interchanging the two variable names in the superscript-$x$ version. Then $\exists x{C}_m^x$ counts at least $m$ distinct satisfying elements without introducing any further variable names. The recursion works on finite and infinite linear orders.

The fragment uses finite conjunction, set-indexed disjunction and existential quantification, with equality and atomic relations. It is preserved under inverse image functors of geometric morphisms. The universal closure of an axiom is expressed by its variable context, not an unrestricted universal-quantifier constructor.

A set of sequents between geometric formulas over a many-sorted signature. Its geometric syntactic category and geometric syntactic topology yield its classifying topos. A model satisfies a sequent when the interpreted antecedent subobject is contained in the consequent in the indicated context.

A geometric theory with only nullary relation symbols has formulas built from primitive propositions by finite conjunctions and set-indexed disjunctions. Its sequents present a frame; its locale carries a canonical model in its sheaf topos, where a proposition is interpreted as the corresponding open subterminal sheaf.

For a commutative ring $R$, this locale is presented by basic opens $U_r$ recording membership in a multiplicatively closed prime filter. Products give intersections. A ring map induces a locale map in the opposite direction. The basic opens satisfy $U_r\vee U_s=1$ exactly when $(r,s)=R$, making unit-ideal calculations a substitute for choosing prime ideals.

A geometric quotient adds geometric sequents over the same signature. Quotients are compared modulo provable equivalence. In a syntactic site the extra sequents become additional covers, giving a subtopos of the original classifying topos. Stronger axioms correspond to a larger site topology and a smaller subtopos.

Objects are geometric formulas in context modulo provable equivalence. Morphisms are provably total, single-valued geometric relations; composition is existential conjunction. Conjunction and equality give finite limits. Interpreting formulas in a model gives a finite-limit-preserving functor, with the additional continuity condition supplied by the geometric syntactic topology.

A family of definable arrows covers a formula when the theory proves that their images jointly exhaust that formula. Such covers encode disjunction and existential quantification. The resulting site presents the classifying topos of the geometric theory. Adding geometric axioms adds covering sieves, yielding the duality between geometric quotients and subtoposes.

A geometric formula is built from atoms by finite conjunction, arbitrary small disjunction and existential quantification. Empty conjunction and disjunction give truth and falsity. In a Grothendieck topos, these constructions use finite limits, unions and images. Formula contexts have finitely many variables.

Regular logic has atomic formulas and equality, truth, finite conjunction and unrestricted existential quantification. Its categorical semantics uses regular categories: conjunction is intersection and existential quantification is image. Disjunction and falsity are not added as formula constructors in the regular fragment.

A regular theory has axioms that are sequents between regular formulas. It has a regular syntactic category and a classifying topos of sheaves for the regular coverage. Its regular formulas enjoy the disjunction property of regular theories when a finite disjunction is allowed as an outer coherent conclusion.

Classically, a regular formula sequent that is not provable has a set-valued countermodel, with empty sorts allowed. Start with the finite diagram of its antecedent, successively adjoin witnesses to the existential consequences of each axiom, and identify elements when equality axioms require it. Every new fact about the original parameters has a finite derivation, so the nonderivable consequent remains false. The filtered union of this witness construction is a model. The conservativity property of this chase construction is studied in Forssell and Lumsdaine's paper.

If a regular theory proves an outer coherent sequent $\varphi ⊢{\bigvee }_{i=1}^n{\psi }_i$ with all formulas regular, it proves $\varphi ⊢{\psi }_i$ for some $i$. In the classifying topos, the corresponding subobjects cover the representable associated with $\varphi$. Irreducibility of that representable and full faithfulness of the syntactic Yoneda embedding produce the desired derivation.

The regular syntactic category has regular formulas-in-context as objects and provably functional regular relations as arrows. It has finite limits and stable image factorizations, with existential quantification supplying images. The regular coverage on this category presents the classifying topos of the theory.

A regular formula is built using the constructors of regular logic, with a finite variable context. The image of a definable relation interprets an existential quantifier. Regular formulas remain regular after substitution, conjunction and existential quantification.

A Cartesian theory uses a many-sorted first-order signature and sequents between Cartesian formulas. The fragment contains equality, atomic relations, truth, finite conjunction and existential quantification with provably unique witnesses. It has a Cartesian syntactic category with finite limits, whose finite-limit-preserving functors classify its internal models. Arbitrary existential quantification, disjunction and falsity are not added as finite-limit constructors.

In the positive finite-limit convention, a Horn theory uses atomic finite-conjunction sequents; uniquely witnessed existential extensions remain Cartesian. Its models are the finite-limit-preserving functors out of its Cartesian syntactic category. This convention does not insert arbitrary existential witnesses or falsity as Cartesian constructors. Its classifier is the presheaf classifier of a Horn theory.

Internal Horn models are finite-limit-preserving functors out of the Cartesian syntactic category. Since that category has finite limits, these are exactly flat functors; the presheaf Diaconescu equivalence for geometric morphisms proves the classifying property. Equivalently the classifier is the covariant functor category on finitely presented set-based models.

Objects are Cartesian formulas-in-context modulo provable equivalence, and arrows are provably total single-valued Cartesian relations. Composition quantifies the unique intermediate tuple. Context concatenation, conjunction and equality give finite limits. Its canonical model interprets a formula as its own context subobject, so factorization of antecedent through consequent is exactly sequent derivability.

If a Cartesian sequent fails to factor its antecedent subobject $A\hookrightarrow C$ through its consequent, the covariant representable functor ${\mathcal{C}}_{\mathbb{T}}(A,-)$ is a set-valued countermodel. It preserves finite limits, and the element named by the antecedent inclusion belongs to the antecedent but cannot belong to the consequent. Hence validity in every set model implies Cartesian derivability.

A Cartesian formula is built from atoms and equality using truth, finite conjunction and uniquely witnessed existential quantification. Uniqueness is proved relative to the theory before admitting the quantifier. In a finite-limit category, such a quantified relation projects monomorphically into the remaining context, so its semantics needs no arbitrary image operation.

Coherent logic uses atomic formulas and equality, finite logical conjunctions and logical disjunctions, truth, falsity and existential quantification. Sequents are universally interpreted in a finite variable context. Its categorical semantics is provided by coherent categories, where conjunction is intersection, disjunction is finite union and existential quantification is image.

When $y$ is not free in $\theta$, the coherent quantifier obeys $\theta \wedge \exists y\varphi ⊣⊢\exists y(\theta \wedge \varphi )$. Categorically this is the interaction of existential images with pullback, ensuring stable image factorizations in a coherent category.

A coherent theory is a first-order signature with a set of coherent sequents as axioms. It has a coherent syntactic category containing a conservative syntactic model. Theories of groups, rings and integral domains admit coherent axiomatizations.

Use the signature of unital commutative rings, its equational axioms, and the coherent sequents $0=1⊢\perp$ and $\top {⊢}_x\mathrm{Inv}(x)\vee \mathrm{Inv}(1-x)$, where $\mathrm{Inv}(x)$ abbreviates $\exists y(xy=1)$. In a set-based model the nonunits form its unique maximal ideal; this is the usual nonzero local ring. In a topos the disjunction expresses local existence of a unit witness. Its classifying topos is defined by the Zariski coverage on finitely presented rings.

A coherent sequent true in all set models of a coherent theory is coherently derivable. A generic underivable sequent remains false after the Boolean cover by a generic quasi-closed subtopos. Slice over its nonzero Boolean counterexample to show classical consistency of the theory with a named tuple satisfying the antecedent and negated consequent. The Henkin construction then gives a set-valued countermodel. This argument does not assume that every Boolean topos has points.

Objects are coherent formulas in context and arrows are provably total, single-valued relations, modulo provable equivalence. Composition existentially eliminates the intermediate tuple. Conjunction constructs finite limits, existential formulas construct images and disjunction constructs finite unions. It is a coherent category.

The canonical model interprets each sort as its truth-context object, each operation by its term graph and each relation by its atomic subobject. A coherent formula is interpreted by its own formula-in-context object. Consequently a coherent sequent holds in this model exactly when it is derivable in the theory.

A coherent sequent is an implication $\varphi {⊢}_{\vec{x}}\psi$ between coherent formulas in a common context. Its semantics is inclusion of the two interpreted subobjects of that context. The context is universally quantified outside the formulas.

A coherent formula is built from atomic relations and equality using $\top$, $\perp$, finite conjunction, finite disjunction and existential quantification. General negation and universal quantification are not constructors. Substitution of well-typed terms preserves coherent formulas.

In first-order logic with logical equality, $s=t$ asserts that the terms denote the same domain element. Logical equality is interpreted as identity rather than as an arbitrary binary predicate. Its natural deduction rules include reflexivity and substitution: equal terms can replace one another in a first-order formula, subject to capture-avoiding substitution. Double-negating logical equality atoms in a Gödel-Gentzen negative translation preserves these rules when the transported translated first-order formula is stable.

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.

When an equality-like symbol is treated as an ordinary binary predicate, no first-order theory consisting of assertions valid for actual identity can force it to be identity. Given a genuine-equality structure on $A$, replace the domain by $A\times \{0,1\}$ and pull all relations back along the projection $\pi$. Lift functions so that $\pi$ commutes with them. Induction on first-order formulas preserves satisfaction because $\pi$ is surjective. Yet the two copies of each point satisfy the equality-like predicate. Thus actual identity must be part of the semantics, or the resulting equivalence classes must be quotiented out.

Intuitionistic first-order logic has the usual introduction and elimination rules for logical connectives, quantifiers and logical equality, but no unrestricted double-negation elimination or law of excluded middle. Its proofs retain the witness and logical disjunction information that can be lost in classical first-order logic.

For an atomic formula $P$ (including logical equality), put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Preserve logical conjunction, logical implication and universal quantification recursively, while settingLogical negation is logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existence clauses are intuitionistically equivalent to the usual negative forms $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$. Every translated first-order formula is stable by stability of a formula under double negation. In classical logic the translation is equivalent to the original first-order formula by mathematical induction and double-negation elimination.

The Gödel-Gentzen negative translation transforms $\Gamma {⊢}_{\mathrm{CL}}A$ into ${\Gamma }^N{⊢}_{\mathrm{IL}}{A}^N$. Induct on a natural deduction derivation. The translated logical conjunction, logical implication and universal rules are ordinary intuitionistic rules. Logical disjunction and existential introduction add double logical negation; their elimination rules first derive the double logical negation of the stable translated conclusion, then use its stability. Classical double-negation elimination translates precisely to stability. If logical equality atoms are double-negated, transport a stable translated conclusion through a logical equality by contradiction and then remove the resulting double logical negation. Original nonlogical axioms must also be translated; the result does not say arbitrary untranslated classical first-order theories are intuitionistically valid.

A first-order formula $A$ is stable when intuitionistic first-order logic proves $\neg \neg A\to A$. Double negations and logical falsity are stable. Logical conjunction of stable first-order formulas is stable; a logical implication is stable when its consequent is stable; and universal quantification preserves stability. For logical implication, from $\neg \neg (A\to B)$ and $A$, assuming $\neg B$ contradicts the first hypothesis, giving $\neg \neg B$ and then $B$. For universality, obtain $\neg \neg A(t)$ from $\neg \neg \forall xA(x)$ for arbitrary $t$, then use stability and generalize.

Classical first-order logic has the quantifier and logical equality rules of natural deduction together with unrestricted double-negation elimination, or equivalently the law of excluded middle. It is interpreted in ordinary two-valued first-order structures.

A first-order formula is built from atomic formulas using logical connectives and quantifiers over the elements of a structure.

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 quantifier prefix followed by a quantifier-free matrix. This does not itself eliminate existential quantifiers.

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

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.

A witness whose existence is asserted separately for each input. The witness need not be the same element for different inputs, so this condition is weaker than existence of a uniform witness.

One element that satisfies a relation simultaneously for every quantified input. A uniform witness also proves the corresponding pointwise statement, because it may be chosen for each particular input.

The quantifier rank of a first-order formula is the maximum nesting depth of quantifiers. Atomic formulas have rank zero; negation preserves rank, binary Boolean connectives take the maximum, and either quantifier increases rank by one. It is not the total number of quantifiers.

Two first-order structures are rank-n equivalent if they agree on all sentences of quantifier rank at most $n$. The tuple version compares formulas at fixed tuples. For finite relational vocabulary this is equivalent to a Duplicator winning strategy in the $n$-round Ehrenfeucht-Fraïssé game.

A primitive positive formula is generated from atomic formulas using only logical conjunction and existential quantification. It can be put in the form $\exists \bar{y}{\bigwedge }_j{\theta }_j(\bar{x},\bar{y})$ with each ${\theta }_j$ atomic. The exam terminology tame formula refers to this fragment. Its reduced product transfer needs only filter intersection and upward closure, together with coordinatewise choices of witnesses.

Existential quantification forms $\exists x\phi (x,\mathbf{y})$. In a first-order structure, it is true at an assignment to $\mathbf{y}$ when some domain element makes the instance true. In natural deduction, elimination uses a fresh variable for the hypothetical witness; that variable may not escape into the conclusion or the remaining undischarged assumptions.

Existence requires at least one witness, not exactly one. Over the natural numbers $\mathbb{N}=\{0,1,2,\dots \}$, $\exists m(m>5)$ is true: $m=6$ works, as do $7,8,\dots$. In intuitionistic first-order logic, a direct proof supplies a witness together with a proof of the corresponding instance; merely rejecting nonexistence is generally weaker.

Placing existential quantification before universal quantification requires a single witness that works throughout:This first-order sentence is false. For any proposed $m$, choose $n=m$: the required inequality becomes $m>m$. For example, $m=3$ works for $n=0,1,2$ but fails at $n=3$. No finite list of successful checks establishes universal quantification over the natural numbers.

An object, or a term denoting an object, that satisfies the predicate asserted by an existential quantification. In a natural deduction use of the existential quantifier elimination rule, a fresh eigenvariable represents an otherwise unspecified witness inside a subproof. The eigenvariable condition prevents it from occurring freely in the exported conclusion or the other undischarged assumptions; violating this restriction is witness escape.

Assume $\forall x(x=c_1\vee \cdots \vee x=c_n)$ with $n\ge 1$. For the forward implication, open a fresh existential witness, instantiate domain exhaustiveness at it, and split into the equality cases. The equality elimination rule transfers its predicate to the corresponding constant, which supplies the required disjunct. Closing the witness scope is legal because the result contains only the named constants. Conversely each named instance gives the existential by the existential quantifier introduction rule, and cases combine those derivations. The constants need not denote distinct objects. A negated named instance can eliminate one case through contradiction and logical falsity elimination rule.

An existential formula is an existential block followed by a quantifier-free formula, with remaining free variables serving as parameters. Truth is preserved by structure embeddings. Reflection of truth for every such formula defines an existential embedding.

Universal quantification forms $\forall x\phi (x,\mathbf{y})$. In a first-order structure, it is true at an assignment to $\mathbf{y}$ when every domain element assigned to $x$ makes the instance true. Its introduction rule requires that the generalized variable not occur freely in undischarged assumptions.

Over the natural numbers, reversing the preceding existential quantification and universal quantification gives a true first-order sentence:Choose $m=n+1$. The computed witnesses for $n=0,1,2,3$ are $m=1,2,3,4$. The choice may depend on the previously given $n$. The formula states that every natural number has a larger natural number; the reversed formula demands one larger than all of them.

The diagram displays a finite window, while the rules $m=n+1$ and $n=m$ settle the two statements for every natural number. This dependence is why quantifier order matters in precise specifications. Choosing one $m$ that works for every $n$ would also provide a witness for each $n$; the reverse inference fails here.

To introduce universal quantification in natural deduction, reason with an arbitrary input, without assuming a special property of it. The construction $m=n+1$ does exactly this and also gives a proof in intuitionistic first-order logic. The introduction and elimination rules for both quantifiers are developed in Frank Pfenning, First-Order Logic and Type Theory, section 4.1.

A universal formula has a block of universal quantifiers followed by a quantifier-free formula. Empty blocks are usually permitted. Truth transfers from a first-order structure to a substructure of a first-order structure for parameters in that substructure: every tuple in the smaller domain is available in the larger domain, and quantifier-free truth is preserved and reflected by the inclusion. This is the dual preservation direction to the forward preservation of an existential formula under a structure embedding.

A quantifier-free first-order formula is built from atomic formulas using logical connectives, with no quantifiers. An embedding of first-order structures preserves and reflects its truth, by mathematical induction on the first-order formula. Both positive and negated atomic information are needed for this conclusion in a relational language.

In a first-order language having at least one closed term, validity of a quantifier-free existential sentence forces inconsistency of the set of negations of all its closed-term instances. Otherwise take a model of those negations and its substructure generated by the closed terms. Quantifier-free truth is preserved there, so the valid existential sentence has a closed-term witness, a contradiction. Compactness then gives a finite disjunction of instances. The nonempty closed-term hypothesis is essential: in a language with no constants or nullary functions, the valid sentence $\exists x(x=x)$ has no closed-term instance.

A quantifier-free sentence is a quantifier-free formula with no free variables. In a language whose only closed group terms denote zero, all quantifier-free sentences have the same truth value in every group, even when existential sentences distinguish them.

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.

An atomic formula containing no variables. In STRIPS, a state records true ground atoms, and the closed-world assumption treats unlisted ground atoms as false. Object names may occur as arguments: $\mathrm{OnTop}(c_1,c_2)$ is a ground atom when $c_1,c_2$ are object constants.

A first-order language specifies its constant, operation, and relation symbols, together with the arity of each nonconstant symbol.

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.

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.

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 constant symbol is a zero-ary function symbol. Its interpretation in a first-order structure names one fixed domain element, and the symbol is a closed term. A language can contain no constant symbols unless a construction explicitly adds them.

A signature specifies the sorts, operation symbols with their input and output sorts, and relation symbols with their input sorts. The logical connectives and quantifiers are supplied separately by the chosen logic. This separates the nonlogical vocabulary from the rules defining a coherent theory.

For coding arithmetic computations, the signature in use is $0,1,+,\times ,<,=$. Bounded remainder tests and polynomial equations use only these symbols. This is a statement about the language: interpretation in the natural numbers does not impose the axioms of a ring.

A first-order term is built recursively from variables and constant symbols by applying function symbols to existing terms. Evaluation in a first-order structure follows the same recursion. An atomic formula applies a relation to terms, or asserts their logical equality.

A first-order structure and an assignment determine the value of every term recursively: a variable has its assigned value, a constant has its interpreted value, and a compound function term is evaluated by applying the interpreted function to the recursively evaluated arguments. This operation supplies the input values for the satisfaction clauses of atomic formulas.

After replacing functions by graph predicates and constants by singleton predicates, $E_t(z)$ says that $z$ is the value of a term $t$. For a unary function graph $P$ and constant predicate $Q$, use $E_x(z)=(z=x)$, $E_c(z)=Q(z)$ and $E_{f(t)}(z)=\exists y(E_t(y)\wedge P(y,z))$. Fresh witnesses avoid variable capture. Totality and uniqueness axioms make each value formula have exactly one witness under every assignment.

A closed term contains no variables, so its value in a first-order structure does not depend on an assignment. In a language containing only relations and the constant zero, zero is the only closed term. A term-generated model has every element denoted by such a term.

A first-order term containing no variables. Constant symbols are ground terms; applying a function symbol to ground terms produces another ground term.

A finite set of formulas mentions only finitely many nonlogical symbols. This observation lets compactness reduce arguments in a language indexed by a large set to a finite sublanguage.