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.

A bounded arithmetic sentence is an arithmetic bounded formula with no free variables. Every quantifier is restricted by an arithmetic first-order term. In the standard natural numbers such a first-order sentence has a definite truth value determined by finite bounded searches.

Let two first-order models satisfy a complete theory and suppose every element of the first is the value of a closed term. Send each such value to the value of the same first-order term in the second first-order model. Completeness decides all logical equality first-order sentences, making this map well-defined and injective. It also decides every logical formula with closed terms substituted, making the map elementary. Thus the first first-order model is prime.

A bounded-complete complete omega-consistent arithmetic first-order theory is correct on every arithmetic first-order sentence. Completeness and first-order consistency make its theoremhood obey the Boolean truth tables. Omega-consistency ensures that every proved existential sentence has a provable standard numeral instance, since otherwise completeness refutes all such instances. Induction on logical formulas now identifies theoremhood with standard truth.

Given a bounded-complete one-consistent arithmetic first-order theory with a false theorem, enumerate first-order sentences and successively choose one-consistent one-sentence extensions. Every stage has Sigma-1 soundness, and a false Sigma-1 theorem in the union would already have a formal proof at one stage. The union is therefore one-consistent and complete while retaining the false theorem. It cannot be omega-consistent, since a complete bounded-complete omega-consistent first-order theory is sound.

A first-order theory whose consequences can be decided by an algorithm that terminates on every input first-order sentence. Decidability of a chosen axiom set alone does not ensure decidability of its consequences.

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.

Two first-order structures are elementarily equivalent when they satisfy the same first-order sentences. They need not be isomorphic or embed into one another. Every elementary embedding implies elementary equivalence of its source and target.

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 existential second-order logic sentence has the formwhere each $R_i$ is a second-order relation variable of fixed finite arity $k_i$ and $\phi$ is a first-order sentence over the input first-order signature expanded by the $R_i$. The first-order sentence may contain both universal quantification and existential quantification over individuals; only the outer quantification over second-order relation variables is required to be existential. Under full semantics for second-order logic, truth means that some expansion by witness relations satisfies $\phi$.

For a fixed existential second-order logic sentence on a domain of cardinality $n$, the witnesses need ${\sum }_{i=1}^m{n}^{k_i}$ membership bits. The arities and the number of witnesses are constants because the sentence is fixed. After guessing those bits, a verifier evaluates the fixed first-order sentence by enumerating assignments to its finitely many individual variables, taking polynomial time. In the second-order encoding of three-colorability, the three witnesses require $3n$ bits, and the edge constraints can be checked over at most $n^2$ ordered vertex pairs. This is the logical form of the NP principle that a positive answer has a short complexity certificate.

The fixed-sentence qualification matters: it is the input first-order structure that varies, rather than an arbitrarily large formula supplied with each input. Fagin's theorem states the converse as well: every isomorphism-invariant NP property of finite relational first-order structures has such a description. The coloring example uses only unary second-order relation variables; the general theorem allows any fixed finite arities.

Fix a finite relational first-order signature $\tau$, and let $\mathcal{K}$ be a class of finite nonempty $\tau$-first-order structures closed under isomorphism. Fagin's theorem states that $\mathcal{K}$ is definable by one existential second-order logic sentence under full semantics for second-order logic if and only if its language of standard finite encodings belongs to NP. A standard encoding numbers the domain $\{0,\dots ,n-1\}$ and lists membership bits for each input relation, together with $n$; take an explicit encoding whose length is at least $n$. The encoding language contains all numbered copies of members of $\mathcal{K}$, with malformed encodings rejected. The isomorphism condition makes membership a property of the structure rather than an arbitrary choice of labels. Changing between the usual explicit encodings preserves the NP characterization by polynomial time translations.

The forward direction is the witness-and-verifier calculation in existential second-order logic. For the reverse direction, the guiding idea is to encode an accepting nondeterministic computation using second-order relation variables: fixed-length tuples of domain elements index enough time steps and storage positions for a polynomial time computation. A first-order sentence checks the initial input, legal transitions, and acceptance. The number of tuples grows with the input, although the checking sentence stays fixed. No total order must be supplied as part of the input first-order signature: an auxiliary total order can itself be existentially guessed and constrained by a first-order sentence. Isomorphism invariance ensures that a change of this auxiliary numbering does not change membership in $\mathcal{K}$.

The second-order encoding of three-colorability is a small instance of the forward direction. The beauty of Fagin's theorem is the complete correspondence: the computational class NP can be characterized by the shape of a logical description, without mentioning a particular machine in the statement. The scope is finite relational first-order structures and fixed sentences; it is not a claim about deciding arbitrary second-order logic sentences or about arbitrary infinite domains.

Ronald Fagin published the result in Generalized First-Order Spectra and Polynomial-Time Recognizable Sets, SIAM-AMS Proceedings 7 (1974), pp. 43–73, Section 4. The original paper frames the correspondence using classes of finite expansions and their encodings. Fagin's author-maintained publication list explains that the abstract in the available copy was added in 2019; its modern summary should therefore not be mistaken for part of the 1974 printing.

A finite axiomatization of a class of structures is a finite set of first-order sentences whose first-order models are exactly that class. The existence of such a set is finite axiomatizability.

A first-order sentence is a formula with no free variables, so its truth in a structure is independent of a variable assignment.

A sentence has no free variables; a first-order sentence is its first-order instance.

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.

Under full semantics for second-order logic, a second-order relation variable of arity $k$ ranges over exactly $\mathcal{P}(D^k)$, the external power set of the appropriate Cartesian product. Thusand universal quantification over $R$ checks every such subset. Here the power set is taken in the ambient mathematical universe, not merely among relations definable by formulas or represented by objects inside $D$.

For $D=\{a,b,c\}$, a unary second-order relation variable has eight possible values, including the three singletons needed by the second-order encoding of three-colorability. The three unary witnesses can range independently over those eight subsets, giving $8^3=512$ candidate triples before the first-order sentence is checked; only six triples pass for the complete graph $K_3$. For $K_4$, there are $16^3=4096$ candidate triples and none passes. Distinguishing the range of candidates from the constraints on valid witnesses clarifies both full semantics for second-order logic and the verifier view of NP.

The appeal of full semantics for second-order logic is its literal reading of assertions about every subset or every relation. A first-order structure fixes the second-order ranges automatically, in contrast to Henkin semantics. That expressive force comes with a limitation: there is no effective, sound deductive system complete for all valid second-order logic sentences under full semantics for second-order logic. This limitation and the change of intended models motivating Henkin semantics are described at the start of ^[ref].

For a domain $V_{\lambda }$, an external functional graph with all its individual ordered pairs in $V_{\lambda }$ is therefore available, even if the whole graph does not belong to $V_{\lambda }$. More generally, a binary second-order relation variable can denote any external subset of $V_{\lambda }\times V_{\lambda }$; its ordered pairs need not themselves be elements of the individual domain. Having endpoints in the domain is what matters. This distinction between internal objects and externally available relations is essential when applying second-order logic to the cumulative hierarchy.

A full set of first-order sentences has existential witnesses among names in its own first-order language: if it proves an existential sentence, it proves some closed-term instance of the matrix. For a deductively closed set this may be stated by membership of the first-order sentences. In a function-free first-order language the witness is a constant symbol. A first-order consistent complete full first-order theory has a canonical term model.

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

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.

An involution partitions its set into fixed points and pairs exchanged by the function. If there is exactly one fixed point, every finite model has odd size. Conversely any finite set of odd size admits such a function by pairing all but one element. The first-order sentence $\forall xf(f(x))=x\wedge \exists z(f(z)=z\wedge \forall x(f(x)=x\to x=z))$ consequently has exactly the positive odd finite model sizes. Its arbitrarily large finite models imply an infinite model by the compactness theorem.

For standard provability satisfying positive introspection, suppose $T⊢{\square }^{j}A\to A$ for some positive integer $j$. Positive introspection gives $T⊢\square A\to {\square }^{j}A$, hence $T⊢\square A\to A$. Löb's theorem yields $T⊢A$. The same argument applies with an already iterated first-order sentence in place of $A$.