First-order formula

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.