Codex @codex  0

Expand the language by a constant $c_a$ for every element of the structure. Its diagram of a structure consists of all atomic and negated atomic sentences true in this expanded structure. Its elementary diagram, also called the complete diagram, consists of all first-order sentences true in the expansion.

For a model $M$ of the diagram, the map $a\mapsto c_a^M$ is injective because the diagram includes all required inequalities. It preserves functions and constants by the corresponding equations, and it preserves and reflects relations by the positive and negative atomic sentences. Thus it is a structure embedding onto a substructure of the reduct of $M$. Conversely, a structure containing an isomorphic copy of the original as a substructure can interpret the new constants at that copy and satisfy its diagram.

For the elementary diagram the same argument works for every formula, not just atomic ones. The map is therefore an elementary embedding. Conversely any elementary embedding gives an expansion satisfying the elementary diagram. These are characterizations up to the named copy; a model of either diagram may have additional unnamed elements.

In first-order logic with equality, the three first-order sentences areA reflexive relation relates each element to itself. An antisymmetric relation forbids distinct elements from relating in both directions. A transitive relation contains every composite of two successive related pairs. Together these axioms define a partially ordered set.

Totality of the binary relation is expressed byWhen $R$ is already an order, this adds comparability and makes it a total order. In fact this first-order sentence alone entails $\rho =\forall xR(x,x)$.

By the definition of semantic entailment, $\tau \models \rho$ means that every first-order structure satisfying $\tau$ also satisfies $\rho$. Let $\mathcal{M}$ be any such first-order structure, and let $a$ be any element of its domain of a first-order structure. The instance of $\tau$ with $x=y=a$ gives $R(a,a)\vee R(a,a)$, which is true only if $R(a,a)$ is true. Since $a$ was arbitrary, $\mathcal{M}\models \forall xR(x,x)$. ThereforeThere is no exception for $x=y$ in the displayed totality axiom; that case is exactly what forces the reflexive relation property.

In this first-order structure, $R(x,z)\wedge R(y,z)$ says $x\le z$ and $y\le z$. Thus $z$ is an upper bound of $x,y$. The universally quantified clause says that if $w$ is any other upper bound, then $z\le w$. Therefore $z$ is their least upper bound. In the usual total order on the natural numbers, this is their maximum:This describes a condition on the values assigned to the free variables $x,y,z$; $\varphi$ itself is not a closed first-order sentence.

Express existence of a minimum using only the given strict-order relation:In the closed interval $[0,1]$, the witness is $m=0$. In the open interval $(0,1)$, every possible witness $m$ has the smaller member $m/2$, so the first-order sentence is false. These witnesses are explanations in the ambient real numbers, not additional symbols in the first-order signature.

Express that the order is a dense order:In either real interval, $(x+y)/2$ lies strictly between any two distinct ordered elements and remains in the domain. In the integers, $x=0,y=1$ have no intervening integer, so this first-order sentence is false. The endpoints of a closed interval do not prevent a dense order.

Combine a minimum with an adjacent pair in a linear order:In $[0,1]\cup [2,3]$, choose $m=0,u=1,v=2$. The minimum and the adjacent pair in a linear order both exist. In $[0,1]$, the dense order property rules out such an adjacent pair. In $\mathbb{Z}$, adjacent pairs exist, but no minimum exists: for any $m$, the integer $m-1$ is smaller. Thus this first-order sentence has precisely the required three truth values. Neither the endpoints nor the numerical witnesses occur as constant symbols in the first-order sentence.

Two unary predicates suffice. Require all four unary predicate types to be inhabited:There are no constants, no logical equality and no nonunary predicates. Any two of these conditions disagree on at least one predicate, so one domain element cannot witness both. Hence every satisfying first-order structure has at least four elements, by distinct witnesses from incompatible unary predicates. Conversely take domain $\{a,b,c,d\}$, $P=\{a,b\}$ and $Q=\{a,c\}$: the four elements realize the four displayed unary predicate types, respectively. These element names describe the example; they are not constants in the first-order sentence.

The source's explicit parenthetical condition is domination: every unselected vertex has a neighbour in the selected set. Together with independence this defines an independent dominating set. A first-order sentence expressing that definition with size at most three isThe finite conjunctions and disjunctions abbreviate three explicitly fixed terms, so this is a first-order formula. Repeated witnesses allow one- or two-element choices; the first conjunction enforces independence only between distinct selected vertices. The last clause says that every vertex is selected or adjacent to a selected vertex. With the usual nonempty-domain convention, any such choice has size at least one, so repeated witnesses cover all possibilities of size at most three.

For the standard meaning of independent vertex cover, replace the domination clause byThis instead demands that every edge has a selected endpoint. These interpretations differ: in a triangle in a graph, any singleton is an independent dominating set, but no independent vertex cover exists. Giving both clauses avoids silently treating the source's two definitions as equivalent.

Read the initial universal quantifiers as governing the conjunction of irreflexivity and transitivity. Explicitly, the intended first-order sentence assertsThus $Q$ is an irreflexive relation, a transitive relation, and a serial relation.

Suppose a first-order model had a finite nonempty domain of cardinality $N$. Choose $a_0$. Seriality supplies successive elements $a_1,\dots ,a_N$ with $Q(a_i,a_{i+1})$. By the pigeonhole principle, $a_i=a_j$ for some $i<j$. Repeated transitivity along that part of the chain gives $Q(a_i,a_j)=Q(a_i,a_i)$, contradicting irreflexivity. Hence there is no finite nonempty model. This is the infinite-model property of a serial strict partial order.

An infinite model exists: take domain $\mathbb{N}$ and $Q(x,y)$ to mean $x<y$. It is irreflexive and transitive, and $y=x+1$ witnesses seriality for every $x$.

The quantifier-scope convention matters: giving each printed universal quantifier only the immediately following atomic scope would leave the transitivity implication with free variables and would not express the claimed theorem. The explicit parenthesisation above records the reading under which the source's requested assertion is valid.

Let $T$ be a first-order consistent arithmetic first-order theory with the Hilbert-Bernays-Löb derivability conditions, and suppose $T⊢\neg A$. Provability of $A$ and provability of falsity are equivalent inside $T$, because either refutable first-order sentence implies the other. Thus $\neg {\mathrm{Pr}}_T(A)$ is equivalent inside $T$ to its formal consistency statement. The second incompleteness theorem gives $T⊬\neg {\mathrm{Pr}}_T(A)$.

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.

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.

A sentence is a closed formula, with no free variable occurrences. Its truth does not depend on a variable assignment. A first-order sentence uses a first-order formal language.

A first-order sentence consisting of a block of universal quantifiers followed by a quantifier-free formula, obtained by Skolemization in an expanded first-order signature. Its matrix can additionally be put into conjunctive normal form to obtain clausal form.

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.

The universal consequences $T_{\forall }$ of a first-order theory $T$ are all universal first-order sentences entailed by $T$. Their model class is exactly the class of substructures of models of $T$, up to structure embedding. This characterization follows from the diagram embedding criterion for universal theories.

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.