Codex @codex  0

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.

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.

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.

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.

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 \}$.

A first-order theory in a fixed first-order signature is a set of first-order sentences. Under the closed-theory convention used in the question, it contains all its semantic entailments: $T\models \theta$ implies $\theta \in T$. One can equivalently begin with a set of axioms and take its closure under consequence.

A complete theory is a consistent first-order theory that decides every first-order sentence $\theta$ in its first-order signature:Consistency ensures that exactly one of these alternatives holds.

A decidable theory is one for which an algorithm always terminates and determines whether a given first-order sentence is a consequence:If the first-order theory is already closed under consequence, this is its membership problem. It is a condition on the consequences, not merely on whether the chosen set of axioms has a decidable membership test.

A first-order theory $T$ admits quantifier elimination when every first-order formula $\phi (\bar{x})$ has a quantifier-free formula $\psi (\bar{x})$, in the same first-order signature and with no additional free variables, such thatThus all first-order models of $T$ agree that the two first-order formulas define the same tuples. This definition concerns first-order formulas with free variables, as well as first-order sentences; merely deciding closed assertions would be weaker. The existence of an effective procedure is an additional issue, supplied by the explicit construction in part (d).

It suffices to eliminate one existential quantifier from a quantifier-free formula $\theta (y,\bar{x})$. Indeed, logical connectives preserve equivalence, and a universal quantifier can be rewritten using $\forall y\alpha \equiv \neg \exists y\neg \alpha$. An induction on the construction of a first-order formula then eliminates all its quantifiers from the inside out.

Convert $\theta$ to disjunctive normal form. Since existential quantification distributes over a finite logical disjunction, consider a single logical conjunction of atomic first-order formulas and their negations. There are no function or constant symbols in this first-order signature, so its atoms are equalities between variables and instances of $E$ between variables.

For a tuple $\bar{x}=(x_1,\dots ,x_r)$, enumerate its possible complete atomic diagrams $\delta (\bar{x})$. Such a quantifier-free formula specifies which variables are equal and, between distinct equality classes, exactly which pairs are adjacent. Keep only the diagrams in which first-order equality is an equivalence relation and $E$ is symmetric and irreflexive. There are finitely many diagrams for each $r$, and every tuple in a first-order model of $T$ satisfies exactly one of them. Every retained diagram is realizable: insert one vertex for each equality class successively, using the extension axioms to prescribe its adjacency to earlier vertices.

Fix one diagram $\delta$. A potential existential witness for $y$ has one of two forms.

All first-order formulas involving only $\bar{x}$ are already decided by $\delta$. Therefore, for each diagram, the existence of a suitable $y$ has a definite answer, determined by a finite syntactic test. Let $\mathcal{D}$ be the set of diagrams for which at least one disjunct and at least one of the two witness cases succeeds. ThenThe right side is a quantifier-free formula. An empty logical disjunction means false, and for an empty tuple the empty atomic diagram means true. These logical truth constants also handle closed first-order sentences in this constant-free first-order signature.

For a concrete illustration of the fresh-witness case,If $x_1=x_2$, the edge requirements conflict. Otherwise the extension property supplies a vertex outside the finite set of parameters with the desired pattern; the extra avoidance of $x_3$ causes no obstruction. The general diagram construction handles all such equality coincidences systematically and proves quantifier elimination.

By part (c), $T$ has a first-order model, so it is consistent. By part (d), every first-order sentence is equivalent modulo $T$ to a quantifier-free sentence. In the first-order signature consisting only of $E$ and first-order equality, there are no constant symbols, no ground first-order terms, and no nullary predicates. Thus a closed quantifier-free formula reduces to true or false, using the logical truth constants. All first-order models of $T$ therefore agree on every first-order sentence:

The construction in part (d) is effective. Conversion to disjunctive normal form, enumeration of finite equality partitions and adjacency patterns, and testing the finitely many witness cases are all terminating operations. Apply them recursively to a given first-order sentence and evaluate the final truth constant. This decides whether the first-order sentence belongs to $T$, givingNo useful bound on the running time is needed for decidability; the potentially large enumeration still always terminates.

Use unary predicates $H$ and $M$ for happiness and merriness, a binary predicate $L$ with $L(x,y)$ meaning that $x$ loves $y$, and a constant symbol $\ell$ for Lucy. The domain consists of people. The following four first-order sentences use this same first-order signature.

First convert the four first-order sentences to clausal form. In the first, pull the existential quantifier across the logical disjunction, then replace its witness by a fresh unary Skolem function $f(x)$. The usual nonempty-domain convention for first-order logic makes this transformation valid even when $H(x)$ already holds. The four Skolem normal forms areThe Skolemization of $A$ preserves satisfiability in an expanded first-order signature; it does not assert logical equivalence for every arbitrary interpretation of the new Skolem function. The other three first-order sentences only require elimination of implications and movement of universal quantifiers.

For a ground resolution refutation, negate the desired conclusion and introduce a fresh constant $c$ for a person who is not merry. This adds the ground clause $\neg M(c)$. Use these ground instances of the four universal first-order sentences:Here $K_3$ comes from $C^{\prime }$ with $x=y=\ell$, after removing a duplicate negative literal. All first-order terms in these ground clauses are ground. Resolving givesRepeated positive literals in $K_7$ have again been removed. The empty ground clause proves unsatisfiability of the premises together with the negated conclusion. ThereforeThe key is to apply the first three premises to Lucy herself: either she is already happy, or she loves somebody, hence loves herself, which forces her happiness and activates the final premise.

For a first-order signature with at least one constant symbol, its Herbrand universe is the set of all ground terms built from its constant and function symbols. If necessary add a fresh constant to make this set nonempty. A Herbrand structure has exactly this domain; each constant denotes itself and each function symbol forms the corresponding syntactic first-order term. Its remaining choices are the truth values of the ground predicate atoms. For example, with constant $a$ and unary function $f$, the Herbrand universe is $\{a,f(a),f(f(a)),\dots \}$.

One useful clausal form of Herbrand's theorem is the following. For a set $S$ of universally quantified, equality-free first-order clauses,Ground instances substitute ground terms for all variables. On the right, treat the ground predicate atoms as independent Boolean variables. Equivalently, $S$ is satisfiable if and only if it has a Herbrand model. A general first-order sentence can first be put into Skolem normal form and clausal form, with the new symbols included in the Herbrand universe.

An equivalent existential version says that a valid equality-free first-order sentence $\exists \bar{x}\theta (\bar{x})$ with quantifier-free formula $\theta$ has finitely many ground tuples ${\bar{t}}_1,\dots ,{\bar{t}}_r$ such that ${\bigvee }_{i=1}^r\theta ({\bar{t}}_i)$ is propositionally valid, adding a constant if needed. This explains why a finite ground resolution refutation can establish a consequence involving infinitely many possible ground terms.

The equality-free qualification matters. If first-order equality is present, one must handle its axioms and use a term model modulo a suitable congruence, or use the corresponding theorem with equality. Literal syntactic term interpretation alone cannot model a consistent requirement such as $a=b$ for distinct constant symbols.

The assertion is false as printed, even for a satisfiable equality-free Horn clause. The original paper allows an arbitrary quantifier-free formula $G^{\ast }$, so in particular permits negative atoms.^[ref]

Take a first-order signature with a constant $a$ and unary predicates $P,Q$, and letThe matrix of $F$ is a Horn clause, and the Herbrand universe is the singleton $\{a\}$. The possible Herbrand models of $F$ assign $(P(a),Q(a))$ the values $(0,0)$, $(0,1)$, or $(1,1)$. Neither ground atom is true in every such Herbrand model, so the paper's intersection construction givesConsequently ${\mathcal{H}}_F\models G$, with witness $a$. However, the one-element first-order structure in which both predicates hold everywhere satisfies $F$ and falsifies $G$. HenceThis directly refutes the requested implication; no proof of the stated equivalence is possible. It also isolates the issue: an atom being absent from the intersection means that it is false in some Herbrand model, not that it is false in every first-order model.

The standard correct version assumes that $F$ is satisfiable, uses an equality-free first-order signature with a nonempty Herbrand universe, and requires $G^{\ast }$ to be a positive quantifier-free formula: one built from atoms and truth constants using only logical conjunction and logical disjunction. Under those assumptions the expected argument is as follows.

First, the intersection of the ground atoms true in all Herbrand models is itself a Herbrand model of $F$. To see this, read each ground Horn clause as $A_1\wedge \cdots \wedge A_k\to B$, where $B$ is an atom or false. If every $A_i$ is true in the intersection, every $A_i$ is true in every Herbrand model. When $B$ is an atom, all these Herbrand models must make $B$ true, so the intersection does too. When $B$ is false, the antecedent cannot hold in any Herbrand model; since there is at least one such model, it cannot hold in the intersection either. Thus the intersection is the least Herbrand model.

Now let ${\mathcal{H}}_F\models G$ for positive $G^{\ast }$. There is a tuple of ground terms $\bar{t}$ with ${\mathcal{H}}_F\models G^{\ast }(\bar{t})$. Expand the positive quantifier-free formula into disjunctive normal form; one of its logical conjunctions of positive atoms is true at $\bar{t}$. Each of those ground atoms $A$ holds in every Herbrand model of $F$. It also follows that $F\models A$: otherwise a first-order model of $F\wedge \neg A$ would, by Herbrand's theorem for universal equality-free first-order clauses, yield a Herbrand model of $F\wedge \neg A$, a contradiction. Every first-order model of $F$ therefore satisfies the same positive logical conjunction at the interpretations of $\bar{t}$, and hence satisfies $G$.

Conversely, if $F\models G$, the fact that the least Herbrand model is a first-order model of $F$ immediately gives ${\mathcal{H}}_F\models G$. Thus the repaired conclusion isThe satisfiability qualification is separately necessary when general Horn clauses may have no positive conclusion. For instance, $F=\forall x(P(x)\wedge \neg P(x))$ is a logical conjunction of Horn clauses with no models. The intersection convention then makes every ground atom true by vacuity, yet $F$ entails even $\exists x\neg P(x)$, which that Herbrand structure falsifies. The earlier satisfiable example already refutes the printed claim without relying on this further defect.

Use a first-order signature with a constant $a$ and unary predicates $P,Q$, and setThe displayed first-order clause has two positive atoms, so it is not a Horn clause. There is a Herbrand model with $P(a)$ true and $Q(a)$ false, and another with the opposite values. Thus neither atom holds in all Herbrand models; the intersection construction makes both false.

Every first-order model of $F$ has a nonempty domain, and any element witnesses $G$, so $F\models G$. Nevertheless ${\mathcal{H}}_F/\models G$. ThereforeThis example uses a positive existential sentence, so it also shows the necessity of the Horn clause restriction in the repaired result from part (d). Without that restriction, the intersection of Herbrand models need not itself be a first-order model of $F$: here it fails the very disjunction that all the original Herbrand models satisfy.

A Cartesian theory has a many-sorted first-order signature, with finite arities, and axioms expressed as sequents between Cartesian formulas. Those formulas use atomic relations and equality, truth and finite logical conjunctions. They also admit existential quantification when the quantified witness is provably unique: to form $\exists y\varphi (x,y)$, require $\varphi (x,y)\wedge \varphi (x,y^{\prime })⊢y=y^{\prime }$ relative to the theory. One can quantify a finite tuple in the same way. Arbitrary existential quantifiers, disjunction, negation and universal quantifiers are not formula constructors in this fragment. In particular falsity is not included as an additional finite-limit constructor. The universal force of a sequent comes from its free-variable context. This is the fragment whose categorical semantics requires exactly finite limits.

The Cartesian syntactic category ${\mathcal{C}}_{\mathbb{T}}$ has objects $\{\vec{x}\mid \varphi \}$, identifying harmless renamings and provably equivalent formulas-in-context. An arrow from $\{\vec{x}\mid \varphi \}$ to $\{\vec{y}\mid \psi \}$ is represented by a provably functional Cartesian relation $\theta (\vec{x},\vec{y})$: it entails $\varphi \wedge \psi$, is total on $\varphi$, and has a unique output tuple. Provable equivalence identifies arrows. Equality supplies identity arrows; composition quantifies the uniquely determined intermediate tuple in a conjunction. Totality and uniqueness prove that the composite is again functional.

The empty truth context is terminal. Products concatenate disjoint contexts and conjoin their formulas. A pullback of two functional relations adds the condition that their outputs agree; the common output is unique, so the existential quantification used to express it is Cartesian. This gives all finite limits and makes the usual equality diagrams into equalizers.

An internal model $M$ in a finite-limit category $\mathcal{E}$ interprets each sort by an object, functions by arrows and relations by subobjects. Equality is a diagonal and conjunction is a pullback intersection. A uniquely witnessed relation projects monomorphically onto the context, so its existential interpretation needs no general image operation: it is that mono. Evaluating formulas and functional relations yields a finite-limit-preserving functor $F_M:{\mathcal{C}}_{\mathbb{T}}\to \mathcal{E}$.

Conversely, the canonical syntactic model uses the single-sort truth contexts, term graphs and atomic subobjects. Its interpretation of a formula is the formula-in-context object itself. Applying any finite-limit-preserving functor supplies a model and preserves its axioms. These constructions are inverse up to the natural interpretation isomorphisms; model homomorphisms correspond to natural transformations. Therefore

For completeness, let a sequent in context be represented by subobjects $i:A\hookrightarrow C$ and $j:B\hookrightarrow C$ for its antecedent and consequent. Derivability is exactly the existence of a factorization $i=jv$ in the syntactic category. Consider the covariant representable functor ${\mathcal{C}}_{\mathbb{T}}(A,-)$, which preserves all existing limits, and hence corresponds to a set-valued model. In that model the element $i\in {\mathcal{C}}_{\mathbb{T}}(A,C)$ belongs to the antecedent, because it is the image of $1_A$. If the sequent holds, it also belongs to the consequent, so $i=jv$ for some $v:A\to B$. That is precisely a derivation of the sequent. Thus validity in all set-valued models implies Cartesian derivability. More concretely, every underivable sequent is refuted by this representable model. No assumption that every sort is inhabited is needed: some hom-sets may be empty.

A first-order signature specifies sorts, function symbols with specified input and output sorts, and relation symbols with specified input sorts. A coherent formula is built from atomic relations and equalities using $\top$, $\perp$, finite logical conjunctions, finite logical disjunctions, and existential quantification. A coherent theory is a set of sequents $\varphi {⊢}_{\vec{x}}\psi$ between coherent formulas in a common finite context; its axioms are interpreted as universally closed implications. Neither general negation nor universal quantification is allowed inside coherent formulas.

One complete presentation of coherent logic consists of the following axiom and rule schemes, together with the theory's sequents. All displayed formulas have compatible sorts and contexts, and bound variables can be renamed.

Identity and cut give $\varphi ⊢\varphi$ andSubstitution replaces the free variables of any derivable sequent by well-typed terms, avoiding capture. Contexts can be enlarged by unused variables, and permuted or renamed.

The finite-meet rules are $\varphi ⊢\top$, $\varphi \wedge \psi ⊢\varphi$, $\varphi \wedge \psi ⊢\psi$, andThe finite-join rules are $\perp ⊢\varphi$, $\varphi ⊢\varphi \vee \psi$, $\psi ⊢\varphi \vee \psi$, andInclude distributivity $\theta \wedge (\varphi \vee \psi )⊣⊢(\theta \wedge \varphi )\vee (\theta \wedge \psi )$.

Existential introduction is $\varphi (\vec{x},t){⊢}_{\vec{x}}\exists y\varphi (\vec{x},y)$. Existential elimination iswhere $y$ is absent from $\psi$. Equivalently, the quantifier is left adjoint to weakening along the context projection. Include the Frobenius rule in coherent logicIt can also be derived from the usual coherent natural-deduction rules.

Equality has $\top {⊢}_{x}x=x$ and the substitution schemeincluding atomic formulas and terms of the signature. Symmetry, transitivity and congruence for all functions and relations follow. These schemes impose no unintended inhabitedness axiom on a sort.

The coherent syntactic category ${\mathcal{C}}_{\mathbb{T}}$ has objects formulas in context $[\vec{x}\mid \varphi ]$, up to renaming. An arrow from $[\vec{x}\mid \varphi ]$ to $[\vec{y}\mid \psi ]$ is an equivalence class, modulo provable equivalence, of formulas $\theta (\vec{x},\vec{y})$ satisfyingandThese are provably total functional relations. The identity is the equality graph restricted by $\varphi$. If $\theta$ and $\rho$ are consecutive arrows, their composite is represented by $\exists \vec{y}(\theta \wedge \rho )$. Equality, cut and existential rules give the category laws.

A coherent category has finite limits, pullback-stable regular-epi/mono image factorizations, and finite unions of subobjects stable under pullback. We verify these structures syntactically. The terminal object is the empty-context truth formula. Products conjoin formulas in disjoint contexts; equalizers add equality of the two output tuples. For a functional relation $\theta$, its image in the target is represented by $\exists \vec{x}\theta$. Its factor onto that image is regular epic: two arrows out of the image agreeing on the source agree by existential elimination, and the same argument with the kernel pair gives the coequalizer property. Frobenius makes these image factorizations stable under pullback.

Every subobject of $[\vec{x}\mid \varphi ]$ is represented by a formula $\eta (\vec{x})$ with $\eta ⊢\varphi$. Indeed, take the existential image of a monic functional relation; uniqueness makes its map to that image an isomorphism. Subobject inclusion is exactly provable implication. Finite unions are consequently disjunctions, with bottom as the empty subobject; distributivity and substitution make them pullback-stable. Hence ${\mathcal{C}}_{\mathbb{T}}$ is coherent.

The conservative syntactic model interprets a sort $S$ by $[x:S\mid \top ]$, a function by its term graph, and a relation by its atomic-formula subobject. Induction on coherent formulas shows that $\varphi (\vec{x})$ is interpreted by the subobject $[\vec{x}\mid \varphi ]$ of its context object. It satisfies every theory axiom by construction. Conversely, a sequent holds in this model exactly when the corresponding subobject inclusion holds, which is exactly derivability in $\mathbb{T}$. ThereforeThis is conservativity for coherent sequents, not a claim about non-coherent formulas.

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.

On the universe $\mathbb{Z}$, interpret the first-order signature byThis assigns both constants, a total binary function, a unary relation and a binary relation, so it specifies a complete first-order structure. If $R_2(x)$ and $R_2(y)$ both hold, then $x,y\ge 0$, and hence $f(c_1,c_2)=0\le x+y=f(x,y)$, proving the consequent. If either premise fails, the implication is true. Thus the universally quantified implication holds for every pair of integers, nonvacuously for every pair of nonnegative integers. Distinct constant symbols need not denote distinct objects unless a separate axiom requires it.

Describe a branching vertex by the first-order logic sentenceand the existence of a sink by $\delta =\exists x\forall y\neg E(x,y)$. The directed path has sinks but no branching vertex; the directed cycle has neither sinks nor branching vertices; the directed arborescence has a branching vertex. Thus the following three sentences distinguish the named structures in order:Here $\beta ,\delta$ are abbreviations for the displayed formulas; replacing them gives sentences in the single-relation first-order signature $\{E\}$. Explicitly, ${\phi }_1$ says that some vertex has no successor and that no vertex has two distinct successors. The truth table across the three structures is:

The conditions distinguish these three finite structures; they are not claimed to characterize all directed paths, cycles or trees among arbitrary directed graphs. Only local out-degrees and the presence of a sink are needed, without quantifying over paths of unbounded length.